]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/grafite/grafiteAst.ml
Matitaweb:
[helm.git] / matitaB / components / grafite / grafiteAst.ml
index 1175d3cc131c7fc9a6083f5ea072c59ad4c1fef4..bc001d173c4b71575b686c78cf470d15be18fa1b 100644 (file)
@@ -32,7 +32,7 @@ type loc = Stdpp.location
 type npattern = 
  NotationPt.term option * (string * NotationPt.term) list * NotationPt.term option
 
-type auto_params = NotationPt.term list option * (string*string) list
+type auto_params = (bool * NotationPt.term list) option * (string*string) list
 
 type ntactic =
    | NApply of loc * NotationPt.term
@@ -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 *)