[obligations] Pre-functionalize Program state

In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.

Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.

This PR is in preparation for the switch to a purely functional state
in #11836 ; the full switch requires deeper changes so it is helpful
to have this PR preparing most of the structure.

Most of the PR is routine; only remarkable change is that the hook for
admitted obligations is now called explicitly in `finish_admitted` as
it had to learn about the different types of proof_endings. Before,
obligations set it in `start_lemma` but only used in the `Admitted`
path.

10 files changed, 377 insertions, 271 deletions

diff --git a/clib/cSig.mli b/clib/cSig.mli
index ca888f875a..1305be42bd 100644
--- a/clib/cSig.mli
+++ b/clib/cSig.mli
@@ -83,6 +83,7 @@ sig
     val min_binding: 'a t -> (key * 'a)
     val max_binding: 'a t -> (key * 'a)
     val choose: 'a t -> (key * 'a)
+    val choose_opt: 'a t -> (key * 'a) option
     val split: key -> 'a t -> 'a t * 'a option * 'a t
     val find: key -> 'a t -> 'a
     val find_opt : key -> 'a t -> 'a option
diff --git a/clib/hMap.ml b/clib/hMap.ml
index 3baa105fb0..210c48786b 100644
--- a/clib/hMap.ml
+++ b/clib/hMap.ml
@@ -356,6 +356,10 @@ struct
     let (_, m) = Int.Map.choose s in
     Map.choose m
 
+  let choose_opt s =
+    try Some (choose s)
+    with Not_found -> None
+
   let find k s =
     let h = M.hash k in
     let m = Int.Map.find h s in
diff --git a/stm/stm.ml b/stm/stm.ml
index b296f8f08f..aa5a14c7dd 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -202,7 +202,7 @@ let mkTransCmd cast cids ceff cqueue =
 (* Parts of the system state that are morally part of the proof state *)
 let summary_pstate = Evarutil.meta_counter_summary_tag,
                      Evd.evar_counter_summary_tag,
-                     DeclareObl.program_tcc_summary_tag
+                     DeclareObl.State.prg_tag
 
 type cached_state =
   | EmptyState
@@ -878,7 +878,7 @@ end = struct (* {{{ *)
     Vernacstate.LemmaStack.t option *
     int *                                   (* Evarutil.meta_counter_summary_tag *)
     int *                                   (* Evd.evar_counter_summary_tag *)
-    DeclareObl.ProgramDecl.t CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
+    DeclareObl.State.t
 
   type partial_state =
     [ `Full of Vernacstate.t
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 9ea54f5d8f..b2f9383f8c 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -238,43 +238,92 @@ let err_not_transp () = pperror not_transp_msg
 
 module ProgMap = Id.Map
 
-let from_prg, program_tcc_summary_tag =
-  Summary.ref_tag ProgMap.empty ~name:"program-tcc-table"
+module StateFunctional = struct
+
+  type t = ProgramDecl.t CEphemeron.key ProgMap.t
+
+  let _empty = ProgMap.empty
+
+  let pending pm =
+    ProgMap.filter
+      (fun _ v -> (CEphemeron.get v).prg_obligations.remaining > 0)
+      pm
+
+  let num_pending pm = pending pm |> ProgMap.cardinal
+
+  let first_pending pm =
+    pending pm |> ProgMap.choose_opt
+    |> Option.map (fun (_, v) -> CEphemeron.get v)
+
+  let get_unique_open_prog pm name : (_, Id.t list) result =
+    match name with
+    | Some n ->
+      Option.cata
+        (fun p -> Ok (CEphemeron.get p))
+        (Error []) (ProgMap.find_opt n pm)
+    | None -> (
+      let n = num_pending pm in
+      match n with
+      | 0 -> Error []
+      | 1 -> Option.cata (fun p -> Ok p) (Error []) (first_pending pm)
+      | _ ->
+        let progs = Id.Set.elements (ProgMap.domain pm) in
+        Error progs )
+
+  let add t key prg = ProgMap.add key (CEphemeron.create prg) t
+
+  let fold t ~f ~init =
+    let f k v acc = f k (CEphemeron.get v) acc in
+    ProgMap.fold f t init
+
+  let all pm = ProgMap.bindings pm |> List.map (fun (_,v) -> CEphemeron.get v)
+  let find m t = ProgMap.find_opt t m |> Option.map CEphemeron.get
+end
 
-(* In all cases, the use of the map is read-only so we don't expose the ref *)
-let get_prg_info_map () = !from_prg
+module State = struct
+
+  type t = StateFunctional.t
+
+  open StateFunctional
+
+  let prg_ref, prg_tag =
+    Summary.ref_tag ProgMap.empty ~name:"program-tcc-table"
 
+  let num_pending () = num_pending !prg_ref
+  let first_pending () = first_pending !prg_ref
+  let get_unique_open_prog id = get_unique_open_prog !prg_ref id
+  let add id prg = prg_ref := add !prg_ref id prg
+  let fold ~f ~init = fold !prg_ref ~f ~init
+  let all () = all !prg_ref
+  let find id = find !prg_ref id
+
+end
+
+(* In all cases, the use of the map is read-only so we don't expose the ref *)
 let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
 
-let check_can_close sec =
-  if not (ProgMap.is_empty !from_prg) then
-    let keys = map_keys !from_prg in
+let check_solved_obligations ~what_for : unit =
+  if not (ProgMap.is_empty !State.prg_ref) then
+    let keys = map_keys !State.prg_ref in
+    let have_string = if Int.equal (List.length keys) 1 then " has " else " have " in
     CErrors.user_err ~hdr:"Program"
       Pp.(
         str "Unsolved obligations when closing "
-        ++ Id.print sec ++ str ":" ++ spc ()
+        ++ what_for ++ 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" ))
+        ++ str have_string
+        ++ str "unsolved obligations" )
 
 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 progmap_remove pm prg = ProgMap.remove prg.prg_name pm
+let progmap_replace prg' pm = map_replace prg'.prg_name prg' pm
 let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0
 
 let obligations_message rem =
-  if rem > 0 then
-    if Int.equal rem 1 then
-      Flags.if_verbose Feedback.msg_info
-        Pp.(int rem ++ str " obligation remaining")
-    else
-      Flags.if_verbose Feedback.msg_info
-        Pp.(int rem ++ str " obligations remaining")
-  else
-    Flags.if_verbose Feedback.msg_info Pp.(str "No more obligations remaining")
+  Format.asprintf "%s %s remaining"
+    (if rem > 0 then string_of_int rem else "No more")
+    (CString.plural rem "obligation")
+  |> Pp.str |> Flags.if_verbose Feedback.msg_info
 
 type progress = Remain of int | Dependent | Defined of GlobRef.t
 
@@ -366,11 +415,12 @@ let declare_definition prg =
   let fix_exn = Hook.get get_fix_exn () in
   let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
   (* XXX: This is doing normalization twice *)
-  let () = progmap_remove prg in
   let kn =
     Declare.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls
       ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma
   in
+  let pm = progmap_remove !State.prg_ref prg in
+  State.prg_ref := pm;
   kn
 
 let rec lam_index n t acc =
@@ -448,25 +498,28 @@ let declare_mutual_definition l =
   (* Only for the first constant *)
   let dref = List.hd kns in
   Declare.Hook.(call ?hook:first.prg_hook { S.uctx = first.prg_ctx; obls; scope; dref });
-  List.iter progmap_remove l;
+  let pm = List.fold_left progmap_remove !State.prg_ref l in
+  State.prg_ref := pm;
   dref
 
 let update_obls prg obls rem =
   let prg_obligations = { obls; remaining = rem } in
   let prg' = {prg with prg_obligations} in
-  progmap_replace prg';
+  let pm = progmap_replace prg' !State.prg_ref in
+  State.prg_ref := pm;
   obligations_message rem;
   if rem > 0 then Remain rem
   else
     match prg'.prg_deps with
     | [] ->
       let kn = declare_definition prg' in
-      progmap_remove prg';
+      let pm = progmap_remove !State.prg_ref prg' in
+      State.prg_ref := pm;
       Defined kn
     | l ->
       let progs =
         List.map
-          (fun x -> CEphemeron.get (ProgMap.find x !from_prg))
+          (fun x -> CEphemeron.get (ProgMap.find x pm))
           prg'.prg_deps
       in
       if List.for_all (fun x -> obligations_solved x) progs then
@@ -487,20 +540,27 @@ let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto =
   let obls = Array.copy obls in
   let () = obls.(num) <- obl in
   let prg = { prg with prg_ctx = uctx } in
-  let () = ignore (update_obls prg obls (pred rem)) in
-  if pred rem > 0 then begin
-    let deps = dependencies obls num in
-    if not (Int.Set.is_empty deps) then
-      ignore (auto (Some prg.prg_name) deps None)
-  end
-
-type obligation_qed_info =
-  { name : Id.t
-  ; num : int
-  ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress
-  }
-
-let obligation_terminator entries uctx { name; num; auto } =
+  let _progress = update_obls prg obls (pred rem) in
+  let () =
+    if pred rem > 0 then
+      let deps = dependencies obls num in
+      if not (Int.Set.is_empty deps) then
+        let _progress = auto (Some prg.prg_name) deps None in
+        ()
+      else ()
+    else ()
+  in
+  ()
+
+type obligation_resolver =
+     Id.t option
+  -> Int.Set.t
+  -> unit Proofview.tactic option
+  -> progress
+
+type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver}
+
+let obligation_terminator entries uctx {name; num; auto} =
   match entries with
   | [entry] ->
     let env = Global.env () in
@@ -509,7 +569,7 @@ let obligation_terminator entries uctx { name; num; auto } =
     let sigma = Evd.from_ctx uctx in
     Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body);
     (* Declare the obligation ourselves and drop the hook *)
-    let prg = CEphemeron.get (ProgMap.find name !from_prg) in
+    let prg = Option.get (State.find name) in
     let { obls; remaining=rem } = prg.prg_obligations in
     let obl = obls.(num) in
     let status =
@@ -533,13 +593,15 @@ let obligation_terminator entries uctx { name; num; auto } =
         (* We merge the new universes and constraints of the
            polymorphic obligation with the existing ones *)
         UState.union prg.prg_ctx uctx
-      else
+      else if
         (* The first obligation, if defined,
            declares the univs of the constant,
            each subsequent obligation declares its own additional
            universes and constraints if any *)
-        if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
-        else uctx
+        defined
+      then
+        UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
+      else uctx
     in
     update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto
   | _ ->
@@ -549,16 +611,21 @@ let obligation_terminator entries uctx { name; num; auto } =
           "[obligation_terminator] close_proof returned more than one proof \
            term")
 
-(* Similar to the terminator but for interactive paths, as the
-   terminator is only called in interactive proof mode *)
-let obligation_hook prg obl num auto { Declare.Hook.S.uctx = ctx'; dref; _ } =
-  let { obls; remaining=rem } = prg.prg_obligations in
+(* Similar to the terminator but for the admitted path; this assumes
+   the admitted constant was already declared.
+
+   FIXME: There is duplication of this code with obligation_terminator
+   and Obligations.admit_obligations *)
+let obligation_admitted_terminator {name; num; auto} ctx' dref =
+  let prg = Option.get (State.find name) in
+  let {obls; remaining = rem} = prg.prg_obligations in
+  let obl = obls.(num) in
   let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in
   let transparent = evaluable_constant cst (Global.env ()) in
-  let () = match obl.obl_status with
-      (true, Evar_kinds.Expand)
-    | (true, Evar_kinds.Define true) ->
-       if not transparent then err_not_transp ()
+  let () =
+    match obl.obl_status with
+    | true, Evar_kinds.Expand | true, Evar_kinds.Define true ->
+      if not transparent then err_not_transp ()
     | _ -> ()
   in
   let inst, ctx' =
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 03f0a57bcb..0e56475326 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -74,19 +74,14 @@ module ProgramDecl : sig
     -> Names.Id.t list
     -> fixpoint_kind option
     -> Vernacexpr.decl_notation list
-    -> ( Names.Id.t
-         * Constr.types
-         * Evar_kinds.t Loc.located
-         * (bool * Evar_kinds.obligation_definition_status)
-         * Int.Set.t
-         * unit Proofview.tactic option )
-      array
+    -> RetrieveObl.obligation_info
     -> (Constr.constr -> Constr.constr)
     -> t
 
   val set_uctx : uctx:UState.t -> t -> t
 end
 
+(** [declare_obligation] Save an obligation *)
 val declare_obligation :
      ProgramDecl.t
   -> Obligation.t
@@ -94,9 +89,29 @@ val declare_obligation :
   -> Constr.types option
   -> Entries.universes_entry
   -> bool * Obligation.t
-(** [declare_obligation] Save an obligation *)
 
-module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set
+module State : sig
+
+  val num_pending : unit -> int
+  val first_pending : unit -> ProgramDecl.t option
+
+  (** Returns [Error duplicate_list] if not a single program is open *)
+  val get_unique_open_prog :
+    Id.t option -> (ProgramDecl.t, Id.t list) result
+
+  (** Add a new obligation *)
+  val add : Id.t -> ProgramDecl.t -> unit
+
+  val fold : f:(Id.t -> ProgramDecl.t -> 'a -> 'a) -> init:'a -> 'a
+
+  val all : unit -> ProgramDecl.t list
+
+  val find : Id.t -> ProgramDecl.t option
+
+  (* Internal *)
+  type t
+  val prg_tag : t Summary.Dyn.tag
+end
 
 val declare_definition : ProgramDecl.t -> Names.GlobRef.t
 
@@ -109,54 +124,50 @@ type progress =
   | Defined of GlobRef.t
   (** Defined as id *)
 
+type obligation_resolver =
+     Id.t option
+  -> Int.Set.t
+  -> unit Proofview.tactic option
+  -> progress
+
 type obligation_qed_info =
   { name : Id.t
   ; num : int
   ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress
   }
 
-val obligation_terminator
-  : Evd.side_effects Declare.proof_entry list
-  -> UState.t
-  -> obligation_qed_info -> unit
 (** [obligation_terminator] part 2 of saving an obligation, proof mode *)
-
-val obligation_hook
-  : ProgramDecl.t
-  -> Obligation.t
-  -> Int.t
-  -> (Names.Id.t option -> Int.Set.t -> 'a option -> 'b)
-  -> Declare.Hook.S.t
+val obligation_terminator :
+    Evd.side_effects Declare.proof_entry list
+  -> UState.t
+  -> obligation_qed_info
   -> unit
-(** [obligation_hook] part 2 of saving an obligation, non-interactive mode *)
 
+(** [obligation_admitted_terminator] part 2 of saving an obligation, non-interactive mode *)
+val obligation_admitted_terminator :
+  obligation_qed_info -> UState.t -> GlobRef.t -> unit
+
+(** [update_obls prg obls n progress] What does this do? *)
 val update_obls :
      ProgramDecl.t
   -> Obligation.t array
   -> int
   -> progress
-(** [update_obls prg obls n progress] What does this do? *)
-
-(** { 2 Util }  *)
 
-(** Check obligations are properly solved before closing a section *)
-val check_can_close : Id.t -> unit
+(** Check obligations are properly solved before closing the
+   [what_for] section / module *)
+val check_solved_obligations : what_for:Pp.t -> unit
 
-val get_prg_info_map : unit -> ProgramDecl.t CEphemeron.key ProgMap.t
-
-val program_tcc_summary_tag :
-  ProgramDecl.t CEphemeron.key Id.Map.t Summary.Dyn.tag
+(** { 2 Util }  *)
 
 val obl_substitution :
      bool
   -> Obligation.t array
   -> Int.Set.t
-  -> (ProgMap.key * (Constr.types * Constr.types)) list
+  -> (Id.t * (Constr.types * Constr.types)) list
 
 val dependencies : Obligation.t array -> int -> Int.Set.t
-
 val err_not_transp : unit -> unit
-val progmap_add : ProgMap.key -> ProgramDecl.t CEphemeron.key -> unit
 
 (* This is a hack to make it possible for Obligations to craft a Qed
  * behind the scenes.  The fix_exn the Stm attaches to the Future proof
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 838496c595..c2e6ae9a5a 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -287,10 +287,14 @@ let compute_proof_using_for_admitted proof typ pproofs =
     | _ -> None
 
 let finish_admitted ~info ~uctx pe =
-  let _r : Names.GlobRef.t list = MutualEntry.declare_variable ~info ~uctx pe in
-  ()
-
-let save_lemma_admitted ~(lemma : t) : unit =
+  let cst = MutualEntry.declare_variable ~info ~uctx pe in
+  (* If the constant was an obligation we need to update the program map *)
+  match CEphemeron.get info.Info.proof_ending with
+  | Proof_ending.End_obligation oinfo ->
+    DeclareObl.obligation_admitted_terminator oinfo uctx (List.hd cst)
+  | _ -> ()
+
+let save_lemma_admitted ~(lemma : t) =
   let udecl = Declare.Proof.get_universe_decl lemma.proof in
   let Proof.{ poly; entry } = Proof.data (Declare.Proof.get_proof lemma.proof) in
   let typ = match Proofview.initial_goals entry with
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 30ebf425d0..a1ddd9f3b2 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -9,10 +9,8 @@
 (************************************************************************)
 
 open Printf
-
 open Names
 open Pp
-open CErrors
 open Util
 
 (* For the records fields, opens should go away one these types are private *)
@@ -20,22 +18,42 @@ open DeclareObl
 open DeclareObl.Obligation
 open DeclareObl.ProgramDecl
 
-let pperror ?info cmd = CErrors.user_err ~hdr:"Program" ?info cmd
-let error s = pperror (str s)
-
 let reduce c =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota env sigma (EConstr.of_constr c))
 
-exception NoObligations of Id.t option
-
 let explain_no_obligations = function
     Some ident -> str "No obligations for program " ++ Id.print ident
   | None -> str "No obligations remaining"
 
-let assumption_message = Declare.assumption_message
+module Error = struct
+
+  let no_obligations n =
+    CErrors.user_err (explain_no_obligations n)
+
+  let ambiguous_program id ids =
+    CErrors.user_err
+      Pp.(str "More than one program with unsolved obligations: " ++ prlist Id.print ids
+          ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print id ++ str "\"")
+
+  let unknown_obligation num =
+    CErrors.user_err (Pp.str (sprintf "Unknown obligation number %i" (succ num)))
 
+  let already_solved num =
+    CErrors.user_err
+      ( str "Obligation" ++ spc () ++ int num ++ str "already" ++ spc ()
+        ++ str "solved." )
+
+  let depends num rem =
+    CErrors.user_err
+      ( str "Obligation " ++ int num
+        ++ str " depends on obligation(s) "
+        ++ pr_sequence (fun x -> int (succ x)) rem)
+
+end
+
+let assumption_message = Declare.assumption_message
 let default_tactic = ref (Proofview.tclUNIT ())
 
 let evar_of_obligation o = Evd.make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
@@ -50,62 +68,6 @@ let subst_deps_obl obls obl =
 
 open Evd
 
-let map_cardinal m =
-  let i = ref 0 in
-  ProgMap.iter (fun _ v ->
-      if (CEphemeron.get v).prg_obligations.remaining > 0 then incr i) m;
-  !i
-
-exception Found of ProgramDecl.t CEphemeron.key
-
-let map_first m =
-  try
-    ProgMap.iter (fun _ v ->
-        if (CEphemeron.get v).prg_obligations.remaining > 0 then
-          raise (Found v)) m;
-    assert(false)
-  with Found x -> x
-
-let get_prog name =
-  let prg_infos = get_prg_info_map () in
-    match name with
-        Some n ->
-          (try CEphemeron.get (ProgMap.find n prg_infos)
-           with Not_found -> raise (NoObligations (Some n)))
-      | None ->
-          (let n = map_cardinal prg_infos in
-             match n with
-                 0 -> raise (NoObligations None)
-               | 1 -> CEphemeron.get (map_first prg_infos)
-               | _ ->
-                let progs = Id.Set.elements (ProgMap.domain prg_infos) in
-                let prog = List.hd progs in
-                let progs = prlist_with_sep pr_comma Id.print progs in
-                user_err
-                  (str "More than one program with unsolved obligations: " ++ progs
-                  ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print prog ++ str "\""))
-
-let get_any_prog () =
-  let prg_infos = get_prg_info_map () in
-  let n = map_cardinal prg_infos in
-  if n > 0 then CEphemeron.get (map_first prg_infos)
-  else raise (NoObligations None)
-
-let get_prog_err n =
-  try get_prog n
-  with NoObligations id as exn ->
-    let _, info = Exninfo.capture exn in
-    pperror ~info (explain_no_obligations id)
-
-let get_any_prog_err () =
-  try get_any_prog ()
-  with NoObligations id as exn ->
-    let _, info = Exninfo.capture exn in
-    pperror ~info (explain_no_obligations id)
-
-let all_programs () =
-  ProgMap.fold (fun k p l -> p :: l) (get_prg_info_map ()) []
-
 let is_defined obls x = not (Option.is_empty obls.(x).obl_body)
 
 let deps_remaining obls deps =
@@ -115,7 +77,6 @@ let deps_remaining obls deps =
       else x :: acc)
     deps []
 
-
 let goal_kind = Decls.(IsDefinition Definition)
 let goal_proof_kind = Decls.(IsProof Lemma)
 
@@ -125,19 +86,19 @@ let kind_of_obligation o =
   | Evar_kinds.Expand -> goal_kind
   | _ -> goal_proof_kind
 
-let rec string_of_list sep f = function
-    [] -> ""
-  | x :: [] -> f x
-  | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
-
 (* Solve an obligation using tactics, return the corresponding proof term *)
-let warn_solve_errored = CWarnings.create ~name:"solve_obligation_error" ~category:"tactics" (fun err ->
-    Pp.seq [str "Solve Obligations tactic returned error: "; err; fnl ();
-            str "This will become an error in the future"])
+let warn_solve_errored =
+  CWarnings.create ~name:"solve_obligation_error" ~category:"tactics"
+    (fun err ->
+      Pp.seq
+        [ str "Solve Obligations tactic returned error: "
+        ; err
+        ; fnl ()
+        ; str "This will become an error in the future" ])
 
 let solve_by_tac ?loc name evi t poly uctx =
+  (* the status is dropped. *)
   try
-    (* the status is dropped. *)
     let env = Global.env () in
     let body, types, _univs, _, uctx =
       Declare.build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in
@@ -146,7 +107,7 @@ let solve_by_tac ?loc name evi t poly uctx =
   with
   | Refiner.FailError (_, s) as exn ->
     let _ = Exninfo.capture exn in
-    user_err ?loc ~hdr:"solve_obligation" (Lazy.force s)
+    CErrors.user_err ?loc ~hdr:"solve_obligation" (Lazy.force s)
   (* If the proof is open we absorb the error and leave the obligation open *)
   | Proof.OpenProof _ ->
     None
@@ -155,17 +116,24 @@ let solve_by_tac ?loc name evi t poly uctx =
     warn_solve_errored ?loc err;
     None
 
+let get_unique_prog prg =
+  match State.get_unique_open_prog prg with
+  | Ok prg -> prg
+  | Error [] ->
+    Error.no_obligations None
+  | Error ((id :: _) as ids) ->
+    Error.ambiguous_program id ids
+
 let rec solve_obligation prg num tac =
   let user_num = succ num in
   let { obls; remaining=rem } = prg.prg_obligations in
   let obl = obls.(num) in
   let remaining = deps_remaining obls obl.obl_deps in
   let () =
-    if not (Option.is_empty obl.obl_body) then
-      pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.");
-    if not (List.is_empty remaining) then
-      pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
-        ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining));
+    if not (Option.is_empty obl.obl_body)
+    then Error.already_solved user_num;
+    if not (List.is_empty remaining)
+    then Error.depends user_num remaining
   in
   let obl = subst_deps_obl obls obl in
   let scope = Declare.(Global Declare.ImportNeedQualified) in
@@ -174,8 +142,7 @@ let rec solve_obligation prg num tac =
   let evd = Evd.update_sigma_env evd (Global.env ()) in
   let auto n oblset tac = auto_solve_obligations n ~oblset tac in
   let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in
-  let hook = Declare.Hook.make (DeclareObl.obligation_hook prg obl num auto) in
-  let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in
+  let info = Lemmas.Info.make ~proof_ending ~scope ~kind () in
   let poly = prg.prg_poly in
   let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in
   let lemma = fst @@ Lemmas.by !default_tactic lemma in
@@ -184,15 +151,14 @@ let rec solve_obligation prg num tac =
 
 and obligation (user_num, name, typ) tac =
   let num = pred user_num in
-  let prg = get_prog_err name in
+  let prg = get_unique_prog name in
   let { obls; remaining } = prg.prg_obligations in
-    if num >= 0 && num < Array.length obls then
-      let obl = obls.(num) in
-        match obl.obl_body with
-          | None -> solve_obligation prg num tac
-          | Some r -> error "Obligation already solved"
-    else error (sprintf "Unknown obligation number %i" (succ num))
-
+  if num >= 0 && num < Array.length obls then
+    let obl = obls.(num) in
+    match obl.obl_body with
+    | None -> solve_obligation prg num tac
+    | Some r -> Error.already_solved num
+  else Error.unknown_obligation num
 
 and solve_obligation_by_tac prg obls i tac =
   let obl = obls.(i) in
@@ -223,7 +189,7 @@ and solve_obligation_by_tac prg obls i tac =
           if def && not prg.prg_poly then (
             (* Declare the term constraints with the first obligation only *)
             let evd = Evd.from_env (Global.env ()) in
-            let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in
+            let evd = Evd.merge_universe_subst evd (UState.subst ctx) in
             let ctx' = Evd.evar_universe_context evd in
             Some (ProgramDecl.set_uctx ~uctx:ctx' prg))
           else Some prg
@@ -239,45 +205,53 @@ and solve_prg_obligations prg ?oblset tac =
     | Some s -> set := s;
       (fun i -> Int.Set.mem i !set)
   in
-  let prg =
-    Array.fold_left_i (fun i prg x ->
-      if p i then
-        match solve_obligation_by_tac prg obls' i tac with
-        | None -> prg
-        | Some prg ->
-          let deps = dependencies obls i in
-          set := Int.Set.union !set deps;
-          decr rem;
-          prg
-      else prg)
-      prg obls'
+  let (), prg =
+    Array.fold_left_i
+      (fun i ((), prg) x ->
+        if p i then (
+          match solve_obligation_by_tac prg obls' i tac with
+          | None -> (), prg
+          | Some prg ->
+            let deps = dependencies obls i in
+            set := Int.Set.union !set deps;
+            decr rem;
+            (), prg)
+        else (), prg)
+      ((), prg) obls'
   in
   update_obls prg obls' !rem
 
 and solve_obligations n tac =
-  let prg = get_prog_err n in
+  let prg = get_unique_prog n in
     solve_prg_obligations prg tac
 
 and solve_all_obligations tac =
-  ProgMap.iter (fun k v -> ignore(solve_prg_obligations (CEphemeron.get v) tac)) (get_prg_info_map ())
+  State.fold ~init:() ~f:(fun k v () ->
+      let _ = solve_prg_obligations v tac in ())
 
 and try_solve_obligation n prg tac =
-  let prg = get_prog prg in
+  let prg = get_unique_prog prg in
   let {obls; remaining } = prg.prg_obligations in
   let obls' = Array.copy obls in
-    match solve_obligation_by_tac prg obls' n tac with
-    | Some prg' -> ignore(update_obls prg' obls' (pred remaining))
-    | None -> ()
+  match solve_obligation_by_tac prg obls' n tac with
+  | Some prg' ->
+    let _r = update_obls prg' obls' (pred remaining) in
+    ()
+  | None -> ()
 
 and try_solve_obligations n tac =
-  try ignore (solve_obligations n tac) with NoObligations _ -> ()
+  let _ = solve_obligations n tac in
+  ()
 
 and auto_solve_obligations n ?oblset tac : progress =
-  Flags.if_verbose Feedback.msg_info (str "Solving obligations automatically...");
-  try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent
+  Flags.if_verbose Feedback.msg_info
+    (str "Solving obligations automatically...");
+  let prg = get_unique_prog n in
+  solve_prg_obligations prg ?oblset tac
 
 open Pp
-let show_obligations_of_prg ?(msg=true) prg =
+
+let show_obligations_of_prg ?(msg = true) prg =
   let n = prg.prg_name in
   let {obls; remaining} = prg.prg_obligations in
   let showed = ref 5 in
@@ -290,70 +264,99 @@ let show_obligations_of_prg ?(msg=true) prg =
                          let x = subst_deps_obl obls x in
                          let env = Global.env () in
                          let sigma = Evd.from_env env in
-                         Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
-                                   str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++
-                                   hov 1 (Printer.pr_constr_env env sigma x.obl_type ++
-                                            str "." ++ fnl ())))
+                         Feedback.msg_info
+                           ( str "Obligation" ++ spc ()
+                           ++ int (succ i)
+                           ++ spc () ++ str "of" ++ spc () ++ Id.print n ++ str ":" ++ spc ()
+                           ++ hov 1
+                                ( Printer.pr_constr_env env sigma x.obl_type
+                                ++ str "." ++ fnl () ) ) )
                    | Some _ -> ())
       obls
 
-let show_obligations ?(msg=true) n =
-  let progs = match n with
-    | None -> all_programs ()
+let show_obligations ?(msg = true) n =
+  let progs =
+    match n with
+    | None ->
+      State.all ()
     | Some n ->
-        try [ProgMap.find n (get_prg_info_map ())]
-        with Not_found -> raise (NoObligations (Some n))
-  in List.iter (fun x -> show_obligations_of_prg ~msg (CEphemeron.get x)) progs
+      (match State.find n with
+       | Some prg -> [prg]
+       | None -> Error.no_obligations (Some n))
+  in
+  List.iter (fun x -> show_obligations_of_prg ~msg x) progs
 
 let show_term n =
-  let prg = get_prog_err n in
+  let prg = get_unique_prog n in
   let n = prg.prg_name in
   let env = Global.env () in
   let sigma = Evd.from_env env in
-    (Id.print n ++ spc () ++ str":" ++ spc () ++
-             Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
-            ++ Printer.pr_constr_env env sigma prg.prg_body)
+  Id.print n ++ spc () ++ str ":" ++ spc ()
+  ++ Printer.pr_constr_env env sigma prg.prg_type
+  ++ spc () ++ str ":=" ++ fnl ()
+  ++ Printer.pr_constr_env env sigma prg.prg_body
 
-let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl)
-                   ?(impargs=[]) ~poly ?(scope=Declare.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic
-    ?(reduce=reduce) ?hook ?(opaque = false) obls =
+let msg_generating_obl name obls =
+  let len = Array.length obls in
   let info = Id.print name ++ str " has type-checked" in
+  Feedback.msg_info
+    (if len = 0 then info ++ str "."
+     else
+       info ++ str ", generating " ++ int len ++
+       str (String.plural len " obligation"))
+
+let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl)
+    ?(impargs = []) ~poly
+    ?(scope = Declare.Global Declare.ImportDefaultBehavior)
+    ?(kind = Decls.Definition) ?tactic ?(reduce = reduce) ?hook
+    ?(opaque = false) obls =
   let prg = ProgramDecl.make ~opaque name ~udecl term t ~uctx [] None [] obls ~impargs ~poly ~scope ~kind reduce ?hook in
   let {obls;_} = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
-    Flags.if_verbose Feedback.msg_info (info ++ str ".");
+    Flags.if_verbose (msg_generating_obl name) obls;
     let cst = DeclareObl.declare_definition prg in
     Defined cst)
-  else (
-    let len = Array.length obls in
-    let () = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in
-      progmap_add name (CEphemeron.create prg);
-      let res = auto_solve_obligations (Some name) tactic in
-        match res with
-        | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some name)) (); res
-        | _ -> res)
-
-let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic
-                           ~poly ?(scope=Declare.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce)
-    ?hook ?(opaque = false) notations fixkind =
-  let deps = List.map (fun ({ Declare.Recthm.name; _ }, _, _) -> name) l in
-    List.iter
-    (fun ({ Declare.Recthm.name; typ; impargs; _ }, b, obls) ->
-     let prg = ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps (Some fixkind)
-       notations obls ~impargs ~poly ~scope ~kind reduce ?hook
-     in progmap_add name (CEphemeron.create prg)) l;
-    let _defined =
-      List.fold_left (fun finished x ->
-        if finished then finished
+  else
+    let () = Flags.if_verbose (msg_generating_obl name) obls in
+    let () = State.add name prg in
+    let res = auto_solve_obligations (Some name) tactic in
+    match res with
+    | Remain rem ->
+      Flags.if_verbose (show_obligations ~msg:false) (Some name);
+      res
+    | _ -> res
+
+let add_mutual_definitions l ~uctx ?(udecl = UState.default_univ_decl)
+    ?tactic ~poly ?(scope = Declare.Global Declare.ImportDefaultBehavior)
+    ?(kind = Decls.Definition) ?(reduce = reduce) ?hook ?(opaque = false)
+    notations fixkind =
+  let deps = List.map (fun ({Declare.Recthm.name; _}, _, _) -> name) l in
+  let pm =
+    List.fold_left
+      (fun () ({Declare.Recthm.name; typ; impargs; _}, b, obls) ->
+        let prg =
+          ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps
+            (Some fixkind) notations obls ~impargs ~poly ~scope ~kind reduce
+            ?hook
+        in
+        State.add name prg)
+      () l
+  in
+  let pm, _defined =
+    List.fold_left
+      (fun (pm, finished) x ->
+        if finished then (pm, finished)
         else
           let res = auto_solve_obligations (Some x) tactic in
-            match res with
-            | Defined _ ->
-                (* If one definition is turned into a constant,
-                   the whole block is defined. *) true
-            | _ -> false)
-        false deps
-    in ()
+          match res with
+          | Defined _ ->
+            (* If one definition is turned into a constant,
+               the whole block is defined. *)
+            (pm, true)
+          | _ -> (pm, false))
+      (pm, false) deps
+  in
+  pm
 
 let admit_prog prg =
   let {obls; remaining} = prg.prg_obligations in
@@ -365,39 +368,41 @@ let admit_prog prg =
             let x = subst_deps_obl obls x in
             let ctx = UState.univ_entry ~poly:false prg.prg_ctx in
             let kn = Declare.declare_constant ~name:x.obl_name ~local:Declare.ImportNeedQualified
-              (Declare.ParameterEntry (None,(x.obl_type,ctx),None)) ~kind:Decls.(IsAssumption Conjectural)
+              (Declare.ParameterEntry (None, (x.obl_type, ctx), None)) ~kind:Decls.(IsAssumption Conjectural)
             in
               assumption_message x.obl_name;
               obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x
         | Some _ -> ())
       obls;
-    ignore(DeclareObl.update_obls prg obls 0)
+  DeclareObl.update_obls prg obls 0
 
+(* get_any_prog *)
 let rec admit_all_obligations () =
-  let prg = try Some (get_any_prog ()) with NoObligations _ -> None in
+  let prg = State.first_pending () in
   match prg with
   | None -> ()
   | Some prg ->
-    admit_prog prg;
+    let _prog = admit_prog prg in
     admit_all_obligations ()
 
 let admit_obligations n =
   match n with
   | None -> admit_all_obligations ()
   | Some _ ->
-    let prg = get_prog_err n in
-    admit_prog prg
+    let prg = get_unique_prog n in
+    let _ = admit_prog prg in
+    ()
 
 let next_obligation n tac =
   let prg = match n with
-  | None -> get_any_prog_err ()
-  | Some _ -> get_prog_err n
+    | None -> State.first_pending () |> Option.get
+    | Some _ -> get_unique_prog n
   in
   let {obls; remaining} = prg.prg_obligations in
   let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
   let i = match Array.findi is_open obls with
-  | Some i -> i
-  | None -> anomaly (Pp.str "Could not find a solvable obligation.")
+    | Some i -> i
+    | None -> CErrors.anomaly (Pp.str "Could not find a solvable obligation.")
   in
   solve_obligation prg i tac
 
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 89ed4c3498..0cd1ebf5dc 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -132,7 +132,5 @@ val show_obligations : ?msg:bool -> Names.Id.t option -> unit
 val show_term : Names.Id.t option -> Pp.t
 val admit_obligations : Names.Id.t option -> unit
 
-exception NoObligations of Names.Id.t option
-
 val explain_no_obligations : Names.Id.t option -> Pp.t
 val check_program_libraries : unit -> unit
diff --git a/vernac/proof_global.ml b/vernac/proof_global.ml
index 54d1db44a4..0c5bc39020 100644
--- a/vernac/proof_global.ml
+++ b/vernac/proof_global.ml
@@ -10,3 +10,4 @@ let get_proof = Declare.Proof.get_proof
 type opacity_flag = Declare.opacity_flag =
   | Opaque [@ocaml.deprecated "Use [Declare.Opaque]"]
   | Transparent [@ocaml.deprecated "Use [Declare.Transparent]"]
+[@@ocaml.deprecated "Use [Declare.opacity_flag]"]
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 35e625859b..53a6409b22 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -576,10 +576,14 @@ let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt
       let env = Global.env () in
       let sigma = Evd.from_env env in
       Some (snd (Hook.get f_interp_redexp env sigma r)) in
-  let do_definition =
-    ComDefinition.(if program_mode then do_definition_program else do_definition) in
-  do_definition ~name:name.v
-    ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook
+  if program_mode then
+    ComDefinition.do_definition_program ~name:name.v
+      ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook
+  else
+    let () =
+      ComDefinition.do_definition ~name:name.v
+        ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook in
+    ()
 
 (* NB: pstate argument to use combinators easily *)
 let vernac_start_proof ~atts kind l =
@@ -1054,10 +1058,21 @@ let vernac_end_section {CAst.loc; v} =
 let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set
 
 (* Dispatcher of the "End" command *)
+let msg_of_subsection ss id =
+  let kind =
+    match ss with
+    | Lib.OpenedModule (false,_,_,_) -> "module"
+    | Lib.OpenedModule (true,_,_,_) -> "module type"
+    | Lib.OpenedSection _ -> "section"
+    | _ -> "unknown"
+  in
+  Pp.str kind ++ spc () ++ Id.print id
 
 let vernac_end_segment ({v=id} as lid) =
-  DeclareObl.check_can_close lid.v;
-  match Lib.find_opening_node id with
+  let ss = Lib.find_opening_node id in
+  let what_for = msg_of_subsection ss lid.v in
+  DeclareObl.check_solved_obligations ~what_for;
+  match ss with
   | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
   | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid
   | Lib.OpenedSection _ -> vernac_end_section lid