Matitaweb: Bugfix for TeX-macro conversion.

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

diff --git a/matitaB/components/grafite/grafiteAst.ml b/matitaB/components/grafite/grafiteAst.ml
index 1175d3cc131c7fc9a6083f5ea072c59ad4c1fef4..9d4d3490a9ce7b3729b85e50484bf3790b174ad2 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 *)