summaryrefslogtreecommitdiff
path: root/library/states.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /library/states.ml
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'library/states.ml')
-rw-r--r--library/states.ml18
1 files changed, 6 insertions, 12 deletions
diff --git a/library/states.ml b/library/states.ml
index 96a487b1..3cb6da12 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -21,18 +21,12 @@ let unfreeze (fl,fs) =
Lib.unfreeze fl;
Summary.unfreeze_summaries fs
-let (extern_state,intern_state) =
- let ensure_suffix f = CUnix.make_suffix f ".coq" in
- let (raw_extern, raw_intern) =
- extern_intern Coq_config.state_magic_number in
- (fun s ->
- let s = ensure_suffix s in
- raw_extern s (freeze ~marshallable:`Yes)),
- (fun s ->
- let s = ensure_suffix s in
- let paths = Loadpath.get_paths () in
- unfreeze (with_magic_number_check (raw_intern paths) s);
- Library.overwrite_library_filenames s)
+let extern_state s =
+ System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:`Yes)
+
+let intern_state s =
+ unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s);
+ Library.overwrite_library_filenames s
(* Rollback. *)