aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-24 16:27:09 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-24 16:27:09 +0000
commit3206760263873e0dd2553ccf73632461eabfdcc6 (patch)
treeeb0a7a677fe5ec13c737ef11f12a89a9baa40ddd
parentde7abebd102227bda6af04a3078479ea09db1da3 (diff)
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
-rw-r--r--config/coq_config.mli3
-rwxr-xr-xconfigure5
-rw-r--r--library/library.ml4
-rw-r--r--library/states.ml5
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);