type search_kind = [ `Locate | `Hint | `Match | `Elim ]
+type print_kind = [ `Env ]
+
type 'term command =
| Abort
| Baseuri of string option (** get/set base uri *)
| Coercion of 'term
| Redo of int option
| Undo of int option
+ | Print of print_kind
type ('term, 'ident) tactical =
| LocatedTactical of CicAst.location * ('term, 'ident) tactical