diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-29 17:45:27 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-29 17:45:27 +0200 |
| commit | 05ab666a1283de5500dbc0520d18bdb05d95f286 (patch) | |
| tree | 538cb7b07372d4e83a6c7823d5cb59ee54606099 /library/states.ml | |
| parent | 82a618e8a4945752698a7900c8af7a51091f7b1b (diff) | |
Make the interface of System.raw_extern_intern much saner.
There is no reason (any longer?) to create simultaneous closures for
interning and externing files. This patch makes the code more readable
by separating both functions and their signatures.
Diffstat (limited to 'library/states.ml')
| -rw-r--r-- | library/states.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/library/states.ml b/library/states.ml index 4e55f0cdc..3cb6da12e 100644 --- a/library/states.ml +++ b/library/states.ml @@ -21,14 +21,12 @@ let unfreeze (fl,fs) = Lib.unfreeze fl; Summary.unfreeze_summaries fs -let (extern_state,intern_state) = - let (raw_extern, raw_intern) = - extern_intern Coq_config.state_magic_number in - (fun s -> - raw_extern s (freeze ~marshallable:`Yes)), - (fun s -> - unfreeze (with_magic_number_check raw_intern 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. *) |