[obligations] Don't allocate libobjects for obligation info.

Obligations/Program currently allocates a libobject object just to
check that there are no obligations pending at the end of a section.

I think this is not the right use case for libobject, thus we turn the
check into an explicit one at the vernac level.

3 files changed, 12 insertions, 29 deletions

diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 626dcd5d34..c13e884736 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -251,43 +251,22 @@ let get_prg_info_map () = !from_prg
 
 let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
 
-let close sec =
+let check_can_close sec =
   if not (ProgMap.is_empty !from_prg) then
     let keys = map_keys !from_prg in
     CErrors.user_err ~hdr:"Program"
       Pp.(
         str "Unsolved obligations when closing "
-        ++ str sec ++ str ":" ++ spc ()
+        ++ Id.print sec ++ str ":" ++ spc ()
         ++ prlist_with_sep spc (fun x -> Id.print x) keys
         ++ ( str (if Int.equal (List.length keys) 1 then " has " else " have ")
            ++ str "unsolved obligations" ))
 
-let input : ProgramDecl.t CEphemeron.key ProgMap.t -> Libobject.obj =
-  let open Libobject in
-  declare_object
-    { (default_object "Program state") with
-      cache_function = (fun (na, pi) -> from_prg := pi)
-    ; load_function = (fun _ (_, pi) -> from_prg := pi)
-    ; discharge_function =
-        (fun _ ->
-          close "section";
-          None )
-    ; classify_function =
-        (fun _ ->
-          close "module";
-          Dispose ) }
-
-let map_replace k v m =
-  ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
-
-let progmap_remove prg =
-  Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg))
-
-let progmap_add n prg =
-  Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg))
-
-let progmap_replace prg' =
-  Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg))
+let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
+let prgmap_op f = from_prg := f !from_prg
+let progmap_remove prg = prgmap_op (ProgMap.remove prg.prg_name)
+let progmap_add n prg = prgmap_op (ProgMap.add n prg)
+let progmap_replace prg = prgmap_op (map_replace prg.prg_name prg)
 
 let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0
 
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 4e20c7c192..16c0413caf 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -139,6 +139,9 @@ val update_obls :
 
 (** { 2 Util }  *)
 
+(** Check obligations are properly solved before closing a section *)
+val check_can_close : Id.t -> unit
+
 val get_prg_info_map : unit -> ProgramDecl.t CEphemeron.key ProgMap.t
 
 val program_tcc_summary_tag :
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 8a4522296f..d273573270 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -983,7 +983,7 @@ let vernac_begin_section ~poly ({v=id} as lid) =
      to its current value ie noop. *)
   set_bool_option_value_gen ~locality:OptLocal ["Universe"; "Polymorphism"] poly
 
-let vernac_end_section {CAst.loc} =
+let vernac_end_section {CAst.loc; v} =
   Dumpglob.dump_reference ?loc
     (DirPath.to_string (Lib.current_dirpath true)) "<>" "sec";
   Lib.close_section ()
@@ -993,6 +993,7 @@ let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set
 (* Dispatcher of the "End" command *)
 
 let vernac_end_segment ({v=id} as lid) =
+  DeclareObl.check_can_close lid.v;
   match Lib.find_opening_node id with
   | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
   | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid