From 24eccfc6dfec012da081a0891c397f013cc590e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 May 2019 15:58:05 +0200
Subject: Stub code for handling sections in kernel.

For now we only keep a count of the number of open sections, discriminating
between polymorphic and monomorphic ones.
---
 library/lib.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index 1f97424590..367a84409b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -572,6 +572,7 @@ let is_in_section ref =
 (*************)
 (* Sections. *)
 let open_section ~poly id =
+  let () = Global.open_section ~poly in
   let opp = !lib_state.path_prefix in
   let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
   let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
@@ -612,7 +613,7 @@ let close_section () =
   lib_state := { !lib_state with lib_stk = before };
   pop_path_prefix ();
   let newdecls = List.map discharge_item secdecls in
-  Summary.unfreeze_summaries fs;
+  let () = Global.close_section fs in
   List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls
 
 (* State and initialization. *)
-- 
cgit v1.2.3