(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 9
+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_obj *) * int (* arity *)
- | Obj of loc * 'obj
type ('term, 'lazy_term, 'reduction, 'ident) tactical =
| Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
| _ -> 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 *)