diff options
| author | Maxime Dénès | 2020-01-28 10:19:15 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2020-01-28 10:19:15 +0100 |
| commit | 2b4ebc5cd24f131567052d64889b2d24d5cc5ee8 (patch) | |
| tree | 1ab3f569641640b18d0fefea20f928dc3b716e37 | |
| parent | 614643e6fb1b5029d1c2bf50cd51f95d621010cf (diff) | |
| parent | 28baf4c999de8673b1dfcf7e79d454809c72444f (diff) | |
Merge PR #11459: cleanup: Lib.freeze doesn't use its [~marshallable] argument
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes
| -rw-r--r-- | library/lib.ml | 2 | ||||
| -rw-r--r-- | library/lib.mli | 2 | ||||
| -rw-r--r-- | library/states.ml | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 2 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 2 |
5 files changed, 5 insertions, 5 deletions
diff --git a/library/lib.ml b/library/lib.ml index 9cce9b92ad..7f96adeecf 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -500,7 +500,7 @@ let close_section () = type frozen = lib_state -let freeze ~marshallable = !lib_state +let freeze () = !lib_state let unfreeze st = lib_state := st diff --git a/library/lib.mli b/library/lib.mli index 0d03046dc2..1fe72389f6 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -151,7 +151,7 @@ val close_section : unit -> unit type frozen -val freeze : marshallable:bool -> frozen +val freeze : unit -> frozen val unfreeze : frozen -> unit (** Keep only the libobject structure, not the objects themselves *) diff --git a/library/states.ml b/library/states.ml index 0be153d96a..90303a2a5c 100644 --- a/library/states.ml +++ b/library/states.ml @@ -18,7 +18,7 @@ let replace_summary (lib,_) st = lib, st let replace_lib (_,st) lib = lib, st let freeze ~marshallable = - (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable) + (Lib.freeze (), Summary.freeze_summaries ~marshallable) let unfreeze (fl,fs) = Lib.unfreeze fl; diff --git a/stm/stm.ml b/stm/stm.ml index eff2403eca..4c539684e3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2362,7 +2362,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in - st, Lib.freeze ~marshallable:false in + st, Lib.freeze () in let inject_non_pstate (s,l) = Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env () diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 222e9eb825..05e23164b1 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1346,7 +1346,7 @@ let inNotation : notation_obj -> obj = (**********************************************************************) let with_lib_stk_protection f x = - let fs = Lib.freeze ~marshallable:false in + let fs = Lib.freeze () in try let a = f x in Lib.unfreeze fs; a with reraise -> let reraise = CErrors.push reraise in |