X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=0cfdef148ced4dfbae84f8d5f0199516cc86e7a3;hb=1e7b084682623531f0a4b23618c6614c3a0c0436;hp=68350ac7536398a1452e864ecb106e5fdd0f9367;hpb=8b1a49bbee9eea86eb74c040defe701370ca5893;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 68350ac75..0cfdef148 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -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 = 30
 
 type ('term,'obj) command =
   | Index of loc * 'term option (* key *) * UriManager.uri (* value *)
@@ -219,6 +220,7 @@ type ('term,'obj) command =
 type ncommand =
   | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *)
   | NObj of loc * CicNotationPt.term CicNotationPt.obj
+  | NInverter of loc * string * CicNotationPt.term * bool list option * CicNotationPt.term option
   | NUnivConstraint of loc * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
   | NCoercion of loc * string *