From 3206760263873e0dd2553ccf73632461eabfdcc6 Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 24 Jul 2008 16:27:09 +0000
Subject: moved magic numbers to configure (share coq/coqchk)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11254 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 config/coq_config.mli | 3 ++-
 configure             | 5 ++++-
 library/library.ml    | 4 +---
 library/states.ml     | 5 ++---
 4 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/config/coq_config.mli b/config/coq_config.mli
index 54d92c62c..f72fa33c5 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -28,9 +28,10 @@ val osdeplibs : string  (* OS dependant link options for ocamlc *)
 (* val defined : string list  (* options for lib/ocamlpp *) *)
 
 val version : string    (* version number of Coq *)
-val versionsi : string  (* version number of Coq\_SearchIsos *)
 val date : string       (* release date *)
 val compile_date : string (* compile date *)
+val vo_magic_number : int
+val state_magic_number : int
 
 val theories_dirs : string list
 val contrib_dirs : string list
diff --git a/configure b/configure
index adbea2493..c27ff74d1 100755
--- a/configure
+++ b/configure
@@ -7,6 +7,8 @@
 ##################################
 
 VERSION=trunk
+VOMAGIC=08193 
+STATEMAGIC=19764
 DATE="Jun. 2008"
 
 # a local which command for sh
@@ -851,9 +853,10 @@ let best = "$best_compiler"
 let arch = "$ARCH"
 let osdeplibs = "$OSDEPLIBS"
 let version = "$VERSION"
-let versionsi = "$VERSIONSI"
 let date = "$DATE"
 let compile_date = "$COMPILEDATE"
+let vo_magic_number = $VOMAGIC
+let state_magic_number = $STATEMAGIC
 let exec_extension = "$EXE"
 let with_geoproof = ref $with_geoproof
 
diff --git a/library/library.ml b/library/library.ml
index eb2b4f06d..963b61998 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -353,10 +353,8 @@ let (in_import, out_import) =
 
 (*s Loading from disk to cache (preparation phase) *)
 
-let vo_magic_number = 08190 (* trunk *)
-
 let (raw_extern_library, raw_intern_library) =
-  System.raw_extern_intern vo_magic_number ".vo"
+  System.raw_extern_intern Coq_config.vo_magic_number ".vo"
 
 let with_magic_number_check f a =
   try f a
diff --git a/library/states.ml b/library/states.ml
index 7c3953151..c985dcf2c 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -19,10 +19,9 @@ let unfreeze (fl,fs) =
   Lib.unfreeze fl;
   Summary.unfreeze_summaries fs
 
-let state_magic_number = 19764
-
 let (extern_state,intern_state) =
-  let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in
+  let (raw_extern, raw_intern) =
+    extern_intern Coq_config.state_magic_number ".coq" in
   (fun s -> raw_extern s (freeze())),
   (fun s ->
     unfreeze (raw_intern (Library.get_load_paths ()) s);
-- 
cgit v1.2.3