[lib] Remove obsolete state-management function add_frozen_state

AFAICS this function predates modern state-handling; nowadays
summaries are stored by the STM and nobody were using this
information.

4 files changed, 4 insertions, 23 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index c98d4a7f3..187b749b8 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -589,7 +589,6 @@ let start_module interp_modast export id args res fs =
   openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
   let prefix = Lib.start_module export id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
-  Lib.add_frozen_state ();
   if_xml (Hook.get f_xml_start_module) mp;
   mp
 
@@ -629,7 +628,6 @@ let end_module () =
   assert (eq_full_path (fst newoname) (fst oldoname));
   assert (ModPath.equal (mp_of_kn (snd newoname)) mp);
 
-  Lib.add_frozen_state () (* to prevent recaching *);
   if_xml (Hook.get f_xml_end_module) mp;
   mp
 
@@ -701,7 +699,6 @@ let start_modtype interp_modast id args mtys fs =
   openmodtype_info := sub_mty_l;
   let prefix = Lib.start_modtype id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
-  Lib.add_frozen_state ();
   if_xml (Hook.get f_xml_start_module_type) mp;
   mp
 
@@ -719,7 +716,6 @@ let end_modtype () =
   assert (eq_full_path (fst oname) (fst oldoname));
   assert (ModPath.equal (mp_of_kn (snd oname)) mp);
 
-  Lib.add_frozen_state ()(* to prevent recaching *);
   if_xml (Hook.get f_xml_end_module_type) mp;
   mp
 
@@ -894,8 +890,7 @@ let get_library_native_symbols dir =
 let start_library dir =
   let mp = Global.start_library dir in
   openmod_info := default_module_info;
-  Lib.start_compilation dir mp;
-  Lib.add_frozen_state ()
+  Lib.start_compilation dir mp
 
 let end_library_hook = ref ignore
 let append_end_library_hook f =
diff --git a/library/lib.ml b/library/lib.ml
index 9d71a854f..f22f53ead 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -27,7 +27,6 @@ type node =
   | ClosedModule  of library_segment
   | OpenedSection of object_prefix * Summary.frozen
   | ClosedSection of library_segment
-  | FrozenState of Summary.frozen
 
 and library_entry = object_name * node
 
@@ -80,7 +79,6 @@ let classify_segment seg =
     | (_,OpenedModule (ty,_,_,_)) :: _ ->
       user_err ~hdr:"Lib.classify_segment"
         (str "there are still opened " ++ str (module_kind ty) ++ str "s")
-    | (_,FrozenState _) :: stk -> clean acc stk
   in
     clean ([],[],[]) (List.rev seg)
 
@@ -254,10 +252,6 @@ let add_anonymous_leaf ?(cache_first = true) obj =
     cache_object (oname,obj)
   end
 
-let add_frozen_state () =
-  add_anonymous_entry
-    (FrozenState (Summary.freeze_summaries ~marshallable:`No))
-
 (* Modules. *)
 
 let is_opening_node = function
@@ -544,7 +538,6 @@ let discharge_item ((sp,_ as oname),e) =
   match e with
   | Leaf lobj ->
       Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
-  | FrozenState _ -> None
   | ClosedSection _ | ClosedModule _ -> None
   | OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
       anomaly (Pp.str "discharge_item.")
@@ -585,8 +578,7 @@ let freeze ~marshallable =
         | n, ClosedModule _ -> Some (n,ClosedModule [])
         | n, OpenedSection (op, _) ->
                Some(n,OpenedSection(op,Summary.empty_frozen))
-        | n, ClosedSection _ -> Some (n,ClosedSection [])
-        | _, FrozenState _ -> None)
+        | n, ClosedSection _ -> Some (n,ClosedSection []))
       !lib_state.lib_stk in
     { !lib_state with lib_stk }
   | _ ->
@@ -596,8 +588,7 @@ let unfreeze st = lib_state := st
 
 let init () =
   unfreeze initial_lib_state;
-  Summary.init_summaries ();
-  add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *)
+  Summary.init_summaries ()
 
 (* Misc *)
 
diff --git a/library/lib.mli b/library/lib.mli
index 9f9d8c7e5..f47d6e1a5 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -23,7 +23,6 @@ type node =
   | ClosedModule  of library_segment
   | OpenedSection of Libnames.object_prefix * Summary.frozen
   | ClosedSection of library_segment
-  | FrozenState of Summary.frozen
 
 and library_segment = (Libnames.object_name * node) list
 
@@ -61,8 +60,6 @@ val pull_to_head : Libnames.object_name -> unit
    for each of them *)
 val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name
 
-val add_frozen_state : unit -> unit
-
 (** {6 ... } *)
 
 (** The function [contents] gives access to the current entire segment *)
@@ -123,8 +120,6 @@ val end_modtype :
   Libnames.object_name * Libnames.object_prefix *
     Summary.frozen * library_segment
 
-(** [Lib.add_frozen_state] must be called after each of the above functions *)
-
 (** {6 Compilation units } *)
 
 val start_compilation : Names.DirPath.t -> Names.module_path -> unit
diff --git a/library/library.ml b/library/library.ml
index 5a5f99cc5..db05ad2b7 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -575,7 +575,7 @@ let require_library_from_dirpath modrefl export =
     else
       add_anonymous_leaf (in_require (needed,modrefl,export));
     if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl;
-  add_frozen_state ()
+  ()
 
 (* the function called by Vernacentries.vernac_import *)