- | Coercion of loc * UriManager.uri * bool (* add_obj *) * int (* arity *)
- | Obj of loc * 'obj
-
-type ('term, 'lazy_term, 'reduction, 'ident) tactical =
- | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
- | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactical
- | Repeat of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
- | Seq of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list
- (* sequential composition *)
- | Then of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical *
- ('term, 'lazy_term, 'reduction, 'ident) tactical list
- | First of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list
- (* try a sequence of loc * tactical until one succeeds, fail otherwise *)
- | Try of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
- (* try a tactical and mask failures *)
- | Solve of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list
- | Progress of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical