(* First order tactics *)
| Absurd (_, term) -> "absurd" ^ term_pp term
| Apply (_, term) -> "apply " ^ term_pp term
+ | ApplyRule (_, term) -> "apply rule " ^ term_pp term
| ApplyP (_, term) -> "applyP " ^ term_pp term
| ApplyS (_, term, params) ->
"applyS " ^ term_pp term ^ pp_auto_params ~term_pp params
| AutoBatch (_,params) -> "autobatch " ^
pp_auto_params ~term_pp params
| Assumption _ -> "assumption"
- | Cases (_, term, pattern, specs) -> Printf.sprintf "cases " ^ term_pp term ^
- pp_tactic_pattern pattern ^
- pp_intros_specs "names " specs
+ | Cases (_, term, pattern, specs) ->
+ Printf.sprintf "cases %s %s%s"
+ (term_pp term)
+ (pp_tactic_pattern pattern)
+ (pp_intros_specs "names " specs)
| Change (_, where, with_what) ->
Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
| Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids)
| Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
| Coercion (_, t, do_composites, i, j) ->
pp_coercion ~term_pp t do_composites i j
+ | PreferCoercion (_,t) ->
+ "prefer coercion " ^ term_pp t
+ | UnificationHint (_,t) ->
+ "unification hint " ^ term_pp t
| Default (_,what,uris) -> pp_default what uris
| Drop _ -> "drop"
| Include (_,path) -> "include \"" ^ path ^ "\""