X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=5d138bbe06624ed27896cfb0511767ee045448a6;hb=d51f9674886d1e609a6ea792b65871dcde4f6503;hp=6b5344f580b4873aa62b3d5be45916e04d136dbd;hpb=8aa44cb352041dd314011996b4b1a1ff8990a000;p=helm.git

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index 6b5344f58..5d138bbe0 100644
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -84,7 +84,7 @@ type nmacro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 36
+let magic = 37
 
 (* composed magic: term + command magics. No need to change this value *)
 let magic = magic + 10000 * NotationPt.magic
@@ -99,13 +99,14 @@ type inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (*
 type command =
   | Include of loc * inclusion_mode * string (* _,buri,_,path *)
   | UnificationHint of loc * nterm * int (* term, precedence *)
-  | NObj of loc * nterm NotationPt.obj
+  | NObj of loc * nterm NotationPt.obj * bool
   | NDiscriminator of loc * nterm
   | NInverter of loc * string * nterm * bool list option * nterm option
-  | NUnivConstraint of loc * NUri.uri * NUri.uri
+  | NUnivConstraint of loc * bool * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
-  | NCoercion of loc * string * bool * nterm * nterm * (string * nterm) * nterm
-  | NQed of loc
+  | NCoercion of loc * string * bool * 
+      (nterm * nterm * (string * nterm) * nterm) option
+  | NQed of loc * bool
   (* ex lexicon commands *)
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *)