| Cut of loc * 'ident option * 'term
| Decompose of loc * ('term, 'ident) type_spec list * 'ident option * 'ident list
| Demodulate of loc
- | Discriminate of loc * 'term
+ | Destruct of loc * 'term
| Elim of loc * 'term * 'term option * int option * 'ident list
| ElimType of loc * 'term * 'term option * int option * 'ident list
| Exact of loc * 'term
| Generalize of loc * ('term, 'lazy_term, 'ident) pattern * 'ident option
| Goal of loc * int (* change current goal, argument is goal number 1-based *)
| IdTac of loc
- | Injection of loc * 'term
| Intros of loc * int option * 'ident list
| Inversion of loc * 'term
| LApply of loc * bool * int option * 'term list * 'term * 'ident option
| Right of loc
| Ring of loc
| Split of loc
- | Subst of loc * string
+ | Subst of loc
| Symmetry of loc
| Transitivity of loc * 'term
(* Costruttori Aggiunti *)
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 8
+let magic = 10
-type 'obj command =
+type ('term,'obj) command =
+ | Coercion of loc * UriManager.uri * bool (* add_obj *) * int (* arity *)
| Default of loc * string * UriManager.uri list
+ | Drop of loc
| Include of loc * string
+ | Obj of loc * 'obj
+ | Relation of
+ loc * string * 'term * 'term * 'term option * 'term option * 'term option
| Set of loc * string * string
- | Drop of loc
| Print of loc * string
| Qed of loc
- | Coercion of loc * UriManager.uri * bool (* add composites *)
- | Obj of loc * 'obj
type ('term, 'lazy_term, 'reduction, 'ident) tactical =
| Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
| 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
| Dot of loc
| Semicolon of loc
| _ -> false
type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
- | Command of loc * 'obj command
+ | Command of loc * ('term, 'obj) command
| Macro of loc * 'term macro
| Tactical of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
* ('term, 'lazy_term, 'reduction, 'ident) tactical option(* punctuation *)