type search_kind = [ `Locate | `Hint | `Match | `Elim ]
+type print_kind = [ `Env | `Coer ]
+
type 'term command =
| Abort
| Baseuri of string option (** get/set base uri *)
- | Check of 'term
+ | Basedir of string option (** get/set base dir *)
+ | Check of 'term
| Search_pat of search_kind * string (* searches with string pattern *)
| Search_term of search_kind * 'term (* searches with term pattern *)
| Proof
| 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