]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite/grafiteAst.ml
ugly coerc db print
[helm.git] / helm / software / components / grafite / grafiteAst.ml
index 68350ac7536398a1452e864ecb106e5fdd0f9367..8fc37e4c543c430bd4a5ea08ea40a90953cbbee9 100644 (file)
@@ -193,10 +193,11 @@ type ('term,'lazy_term) macro =
 
 type nmacro =
   | NCheck of loc * CicNotationPt.term
+  | Screenshot of loc * string
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 27
+let magic = 28
 
 type ('term,'obj) command =
   | Index of loc * 'term option (* key *) * UriManager.uri (* value *)