commit by user andrea

[helm.git] / matitaB / components / grafite / grafiteAst.ml

diff --git a/matitaB/components/grafite/grafiteAst.ml b/matitaB/components/grafite/grafiteAst.ml
index 1175d3cc131c7fc9a6083f5ea072c59ad4c1fef4..bb496f2c02678a512694bcc6df43ae79853f5256 100644 (file)
--- a/matitaB/components/grafite/grafiteAst.ml
+++ b/matitaB/components/grafite/grafiteAst.ml
@@ -82,15 +82,15 @@ type nmacro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 35
+let magic = 37
 
 (* composed magic: term + command magics. No need to change this value *)
 let magic = magic + 10000 * NotationPt.magic
 
 type alias_spec =
-  | Ident_alias of string * string        (* identifier, uri *)
-  | Symbol_alias of string * int * string (* name, instance no, description *)
-  | Number_alias of int * string          (* instance no, description *)
+  | Ident_alias of string * string  (* identifier, uri *)
+  | Symbol_alias of string * string option * string (* name, uri, description *)
+  | Number_alias of string option * string (* uri, description *)
 
 type inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (* aka aliases *)
 
@@ -103,9 +103,9 @@ type command =
   | NUnivConstraint of loc * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
   | NCoercion of loc * string *
-      NotationPt.term * NotationPt.term *
-      (string * NotationPt.term) * NotationPt.term
-  | NQed of loc
+      (NotationPt.term * NotationPt.term *
+        (string * NotationPt.term) * NotationPt.term) option
+  | NQed of loc * bool
   (* ex lexicon commands *)
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *)