| WLocate of loc * string
| WElim of loc * 'term
(* real macros *)
- | Print of loc * string
| Check of loc * 'term
| Hint of loc
- | Quit of loc
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 5
+let magic = 6
type 'obj command =
| Default of loc * string * UriManager.uri list
| Include of loc * string
| 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