From 28baf4c999de8673b1dfcf7e79d454809c72444f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 27 Jan 2020 17:09:12 +0100
Subject: cleanup: Lib.freeze doesn't use its [~marshallable] argument

---
 library/lib.ml       | 2 +-
 library/lib.mli      | 2 +-
 library/states.ml    | 2 +-
 stm/stm.ml           | 2 +-
 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
-- 
cgit v1.2.3