From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 26 Sep 2005 08:57:00 +0000 (+0000)
Subject: added magic numbers
X-Git-Tag: LAST_BEFORE_NEW~13
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a82fc7fac28ab55650be57a127c3e3230981f72d;p=helm.git

added magic numbers
they must be increased each time the data structures dumped in .moo file are changed!!!!
---

diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml
index bce159937..b0e9762be 100644
--- a/helm/ocaml/cic_notation/cicNotationPt.ml
+++ b/helm/ocaml/cic_notation/cicNotationPt.ml
@@ -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 *)
 
diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml
index 45f7c1aea..350b32a37 100644
--- a/helm/ocaml/cic_notation/grafiteAst.ml
+++ b/helm/ocaml/cic_notation/grafiteAst.ml
@@ -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
-  
+