]> matita.cs.unibo.it Git - helm.git/commitdiff
added magic numbers
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 26 Sep 2005 08:57:00 +0000 (08:57 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 26 Sep 2005 08:57:00 +0000 (08:57 +0000)
they must be increased each time the data structures dumped in .moo file are changed!!!!

helm/ocaml/cic_notation/cicNotationPt.ml
helm/ocaml/cic_notation/grafiteAst.ml

index bce1599373b96c0d3cba5820891fe10741765094..b0e9762bee7646cbd0040ec8e124c214ddb7409b 100644 (file)
@@ -59,6 +59,10 @@ type literal =
 
 type case_indtype = string * href option
 
+(** To be increased each time the term type below changes, used for "safe"
+ * marshalling *)
+let magic = 1
+
 type term =
   (* CIC AST *)
 
index 45f7c1aea7882afbb31bf08374cc27d45dd5f1b1..350b32a37f196457d6f6c5d05a2f37de79159a64 100644 (file)
@@ -136,6 +136,10 @@ type obj =
       (string * Ast.term) list
       (** left parameters, name, type, fields *)
 
+(** To be increased each time the command type below changes, used for "safe"
+ * marshalling *)
+let magic = 1
+
 type ('term,'obj) command =
   | Default of loc * string * UriManager.uri list
   | Include of loc * string
@@ -162,7 +166,10 @@ type ('term,'obj) command =
     (* DEBUGGING *)
   | Render of loc * UriManager.uri (* render library object *)
 
-let reash_uris =
+(* composed magic: term + command magics. No need to change this value *)
+let magic = magic + 10000 * CicNotationPt.magic
+
+let reash_cmd_uris =
   function
   | Default (loc, name, uris) ->
       let uris =
@@ -206,4 +213,4 @@ type dependency =
   | IncludeDep of string
   | BaseuriDep of string
   | UriDep of UriManager.uri
-  
+