Merge PR #11772: [obligations] Don't allocate libobjects for obligation info.

Reviewed-by: ppedrot

4 files changed, 22 insertions, 42 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/obligations.ml b/vernac/obligations.ml
index f449cb02f1..a29ba44907 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -17,11 +17,8 @@ open Printf
    - Apply term prefixed by quantification on "existentials".
 *)
 
-open Term
 open Constr
-open Vars
 open Names
-open Evd
 open Pp
 open CErrors
 open Util
@@ -41,7 +38,7 @@ let check_evars env evm =
     (fun key evi ->
        if Evd.is_obligation_evar evm key then ()
        else
-         let (loc,k) = evar_source key evm in
+         let (loc,k) = Evd.evar_source key evm in
          Pretype_errors.error_unsolvable_implicit ?loc env evm key None)
   (Evd.undefined_map evm)
 
@@ -133,14 +130,14 @@ let etype_of_evar evm evs hyps concl =
             | LocalDef (id,c,_) ->
                 let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in
                 let c' = subst_vars acc 0 c' in
-                  mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
+                Term.mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
                 Int.Set.union s'' s',
                 Id.Set.union trans'' trans'
             | LocalAssum (id,_) ->
-                mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
+              Term.mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
     | [] ->
-        let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in
-          subst_vars acc 0 t', s, trans
+      let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in
+      subst_vars acc 0 t', s, trans
   in aux [] 0 (List.rev hyps)
 
 let trunc_named_context n ctx =
@@ -152,14 +149,14 @@ let rec chop_product n t =
   if Int.equal n 0 then Some t
   else
     match Constr.kind t with
-      | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (pop b) else None
+      | Prod (_, _, b) ->  if Vars.noccurn 1 b then chop_product (pred n) (pop b) else None
       | _ -> None
 
 let evar_dependencies evm oev =
   let one_step deps =
     Evar.Set.fold (fun ev s ->
       let evi = Evd.find evm ev in
-      let deps' = evars_of_filtered_evar_info evm evi in
+      let deps' = Evd.evars_of_filtered_evar_info evm evi in
       if Evar.Set.mem oev deps' then
         invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev)
       else Evar.Set.union deps' s)
@@ -215,13 +212,13 @@ let eterm_obligations env name evm fs ?status t ty =
       (fun (id, (n, nstr), ev) l ->
          let hyps = Evd.evar_filtered_context ev in
          let hyps = trunc_named_context nc_len hyps in
-         let evtyp, deps, transp = etype_of_evar evm l hyps ev.evar_concl in
+         let evtyp, deps, transp = etype_of_evar evm l hyps ev.Evd.evar_concl in
          let evtyp, hyps, chop =
            match chop_product fs evtyp with
            | Some t -> t, trunc_named_context fs hyps, fs
            | None -> evtyp, hyps, 0
          in
-         let loc, k = evar_source id evm in
+         let loc, k = Evd.evar_source id evm in
          let status = match k with
            | Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o
            | _ -> match status with
@@ -282,7 +279,7 @@ let assumption_message = Declare.assumption_message
 
 let default_tactic = ref (Proofview.tclUNIT ())
 
-let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
+let evar_of_obligation o = Evd.make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
 
 let subst_deps expand obls deps t =
   let osubst = DeclareObl.obl_substitution expand obls deps in
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