diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-29 17:05:45 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-29 17:05:45 +0200 |
| commit | 82a618e8a4945752698a7900c8af7a51091f7b1b (patch) | |
| tree | d1d0044005573d11830d264c9eb6802aa9e237a2 /library/states.ml | |
| parent | da4d0b0e3d82621fe8338dd313b788472fc31bb2 (diff) | |
Prevent States.intern_state and System.extern_intern from looking up files in the loadpath.
This patch causes a bit of code duplication (because of the .coq suffix
added to state files) but it makes it clear which part of the code is
looking up files in the loadpath and for what purpose. Also it makes the
interface of System.extern_intern and System.raw_extern_intern much saner.
Diffstat (limited to 'library/states.ml')
| -rw-r--r-- | library/states.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/library/states.ml b/library/states.ml index 96a487b16..4e55f0cdc 100644 --- a/library/states.ml +++ b/library/states.ml @@ -22,16 +22,12 @@ let unfreeze (fl,fs) = 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); + unfreeze (with_magic_number_check raw_intern s); Library.overwrite_library_filenames s) (* Rollback. *) |