Merge PR #12301: [declare] Grand unification of the proof save path.

Reviewed-by: SkySkimmer
Ack-by: ppedrot

32 files changed, 1491 insertions, 1487 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/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh b/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh
deleted file mode 100644
index c584438b21..0000000000
--- a/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10185" ] || [ "$CI_BRANCH" = "instance-no-bang" ]; then
-
-    quickchick_CI_REF=instance-no-bang
-    quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick
-
-fi
diff --git a/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh
deleted file mode 100644
index 8a734feada..0000000000
--- a/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11703" ] || [ "$CI_BRANCH" = "master+turning-numTok-into-a-numeral-API" ]; then
-
-    quickchick_CI_REF=master+adapting-numTok-new-api-pr11703
-    quickchick_CI_GITURL=https://github.com/herbelin/QuickChick
-
-fi
diff --git a/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh
deleted file mode 100644
index 6928925e54..0000000000
--- a/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11731" ] || [ "$CI_BRANCH" = "proof+more_naming_unif" ]; then
-
-    equations_CI_REF=proof+more_naming_unif
-    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    rewriter_CI_REF=proof+more_naming_unif
-    rewriter_CI_GITURL=https://github.com/ejgallego/rewriter
-
-    elpi_CI_REF=proof+more_naming_unif
-    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh b/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh
deleted file mode 100644
index 8dae29adb6..0000000000
--- a/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11812" ] || [ "$CI_BRANCH" = "export-hint-globality" ]; then
-
-    equations_CI_REF="export-hint-globality"
-    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-
-    fiat_parsers_CI_REF="export-hint-globality"
-    fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat
-
-fi
diff --git a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
deleted file mode 100644
index e3a8eb07f3..0000000000
--- a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11818" ] || [ "$CI_BRANCH" = "proof+remove_special_case_first_declaration_in_mutual" ]; then
-
-    metacoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
-    metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
-
-    elpi_CI_REF=proof+remove_special_case_first_declaration_in_mutual
-    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-    paramcoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
-    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
-
-    equations_CI_REF=proof+remove_special_case_first_declaration_in_mutual
-    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh
deleted file mode 100644
index 4170799be7..0000000000
--- a/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11820" ] || [ "$CI_BRANCH" = "partial-import" ]; then
-
-    elpi_CI_REF=partial-import
-    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh
deleted file mode 100644
index cd6b408813..0000000000
--- a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh
+++ /dev/null
@@ -1,24 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "11896" ] || [ "$CI_BRANCH" = "evar-inst-list" ]; then
-
-    coqhammer_CI_REF="evar-inst-list"
-    coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer
-
-    elpi_CI_REF="evar-inst-list"
-    elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
-
-    equations_CI_REF="evar-inst-list"
-    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-
-    metacoq_CI_REF="evar-inst-list"
-    metacoq_CI_GITURL=https://github.com/ppedrot/metacoq
-
-    mtac2_CI_REF="evar-inst-list"
-    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
-
-    quickchick_CI_REF="evar-inst-list"
-    quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick
-
-    unicoq_CI_REF="evar-inst-list"
-    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
-
-fi
diff --git a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
deleted file mode 100644
index 6bee3c7bb6..0000000000
--- a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12023" ] || [ "$CI_BRANCH" = "master+fixing-empty-Ltac-v-file" ]; then
-
-    fiat_crypto_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
-    fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto
-
-    mtac2_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
-    mtac2_CI_GITURL=https://github.com/herbelin/Mtac2
-
-    metacoq_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
-    metacoq_CI_GITURL=https://github.com/herbelin/template-coq
-
-    unimath_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
-    unimath_CI_GITURL=https://github.com/herbelin/UniMath
-
-fi
diff --git a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh
deleted file mode 100644
index b5faabcfe1..0000000000
--- a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12107" ] || [ "$CI_BRANCH" = "no-mod-univs" ]; then
-
-    elpi_CI_REF=no-mod-univs
-    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh b/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh
deleted file mode 100644
index 0f8daf418c..0000000000
--- a/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "12227" ] || [ "$CI_BRANCH" = "refiner-rm-v82" ]; then
-
-    equations_CI_REF="refiner-rm-v82"
-    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-
-fi
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index f09b35a6d1..e5665c59b8 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -40,7 +40,7 @@ let start_deriving f suchthat name : Lemmas.t =
                 TNil sigma))))))
   in
 
-  let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) ~kind () in
+  let info = Lemmas.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
   let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in
   Lemmas.pf_map (Declare.Proof.map_proof begin fun p ->
     Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
diff --git a/stm/stm.ml b/stm/stm.ml
index b296f8f08f..04f08e488b 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
+                     Declare.Obls.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 *)
+    Declare.Obls.State.t
 
   type partial_state =
     [ `Full of Vernacstate.t
@@ -1684,7 +1684,9 @@ end = struct (* {{{ *)
       (* STATE We use the state resulting from reaching start. *)
       let st = Vernacstate.freeze_interp_state ~marshallable:false in
       ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None)));
-      `OK proof
+      (* Is this name the same than the one in scope? *)
+      let name = Declare.get_po_name proof in
+      `OK name
       end
     with e ->
       let (e, info) = Exninfo.capture e in
@@ -1723,7 +1725,7 @@ end = struct (* {{{ *)
     | `ERROR -> exit 1
     | `ERROR_ADMITTED -> cst, false
     | `OK_ADMITTED -> cst, false
-    | `OK { Declare.name } ->
+    | `OK name ->
         let con = Nametab.locate_constant (Libnames.qualid_of_ident name) in
         let c = Global.lookup_constant con in
         let o = match c.Declarations.const_body with
@@ -3308,7 +3310,7 @@ let unreachable_state_hook = Hooks.unreachable_state_hook
 let document_add_hook = Hooks.document_add_hook
 let document_edit_hook = Hooks.document_edit_hook
 let sentence_exec_hook = Hooks.sentence_exec_hook
-let () = Hook.set DeclareObl.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
+let () = Declare.Obls.stm_get_fix_exn := (fun () -> !State.fix_exn_ref)
 
 type document = VCS.vcs
 let backup () = VCS.backup ()
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 55af2e1a7d..21e2afe6a9 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -345,7 +345,7 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term
   let hook = Declare.Hook.make hook in
   let uctx = Evd.evar_universe_context sigma in
   let scope, kind = Declare.Global Declare.ImportDefaultBehavior, Decls.Instance in
-  let _ : DeclareObl.progress =
+  let _ : Declare.Obls.progress =
     Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls
   in ()
 
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 95f3955309..eac8f92e2e 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -127,7 +127,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
   let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in
-  let _ : DeclareObl.progress =
+  let _ : Declare.Obls.progress =
     Obligations.add_definition
       ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls
   in ()
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 4e9e24b119..4aa46e0a86 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -273,7 +273,7 @@ let collect_evars_of_term evd c ty =
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
 let do_program_recursive ~scope ~poly fixkind fixl =
-  let cofix = fixkind = DeclareObl.IsCoFixpoint in
+  let cofix = fixkind = Declare.Obls.IsCoFixpoint in
   let (env, rec_sign, udecl, evd), fix, info =
     interp_recursive ~cofix ~program_mode:true fixl
   in
@@ -314,8 +314,8 @@ let do_program_recursive ~scope ~poly fixkind fixl =
   end in
   let uctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
-  | DeclareObl.IsFixpoint _ -> Decls.Fixpoint
-  | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint
+  | Declare.Obls.IsFixpoint _ -> Decls.Fixpoint
+  | Declare.Obls.IsCoFixpoint -> Decls.CoFixpoint
   in
   let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
   Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind
@@ -345,7 +345,7 @@ let do_fixpoint ~scope ~poly l =
     | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
       let annots = List.map (fun fix ->
           Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
-      let fixkind = DeclareObl.IsFixpoint annots in
+      let fixkind = Declare.Obls.IsFixpoint annots in
       let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
       do_program_recursive ~scope ~poly fixkind l
 
@@ -355,4 +355,4 @@ let do_fixpoint ~scope ~poly l =
 
 let do_cofixpoint ~scope ~poly fixl =
   let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in
-  do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl
+  do_program_recursive ~scope ~poly Declare.Obls.IsCoFixpoint fixl
diff --git a/vernac/declare.ml b/vernac/declare.ml
index c3f95c5297..c291890dce 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -120,7 +120,7 @@ let get_open_goals ps =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
   List.length shelf
 
-type import_status = ImportDefaultBehavior | ImportNeedQualified
+type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeedQualified
 
 (** Declaration of constants and parameters *)
 
@@ -155,6 +155,8 @@ type proof_object =
   ; uctx: UState.t
   }
 
+let get_po_name { name } = name
+
 let private_poly_univs =
   Goptions.declare_bool_option_and_ref
     ~depr:false
@@ -847,23 +849,6 @@ let get_current_context pf =
   let p = get_proof pf in
   Proof.get_proof_context p
 
-module Proof = struct
-  type nonrec t = t
-  let get_proof = get_proof
-  let get_proof_name = get_proof_name
-  let get_used_variables = get_used_variables
-  let get_universe_decl = get_universe_decl
-  let get_initial_euctx = get_initial_euctx
-  let map_proof = map_proof
-  let map_fold_proof = map_fold_proof
-  let map_fold_proof_endline = map_fold_proof_endline
-  let set_endline_tactic = set_endline_tactic
-  let set_used_variables = set_used_variables
-  let compact = compact_the_proof
-  let update_global_env = update_global_env
-  let get_open_goals = get_open_goals
-end
-
 let declare_definition_scheme ~internal ~univs ~role ~name c =
   let kind = Decls.(IsDefinition Scheme) in
   let entry = pure_definition_entry ~univs c in
@@ -876,7 +861,7 @@ let _ = Abstract.declare_abstract := declare_abstract
 
 let declare_universe_context = DeclareUctx.declare_universe_context
 
-type locality = Discharge | Global of import_status
+type locality = Locality.locality = | Discharge | Global of import_status
 
 (* Hooks naturally belong here as they apply to both definitions and lemmas *)
 module Hook = struct
@@ -1053,3 +1038,982 @@ let prepare_parameter ~poly ~udecl ~types sigma =
 
 (* Compat: will remove *)
 exception AlreadyDeclared = DeclareUniv.AlreadyDeclared
+
+module Obls = struct
+
+open Constr
+
+type 'a obligation_body = DefinedObl of 'a | TermObl of constr
+
+module Obligation = struct
+  type t =
+    { obl_name : Id.t
+    ; obl_type : types
+    ; obl_location : Evar_kinds.t Loc.located
+    ; obl_body : pconstant obligation_body option
+    ; obl_status : bool * Evar_kinds.obligation_definition_status
+    ; obl_deps : Int.Set.t
+    ; obl_tac : unit Proofview.tactic option }
+
+  let set_type ~typ obl = {obl with obl_type = typ}
+  let set_body ~body obl = {obl with obl_body = Some body}
+end
+
+type obligations = {obls : Obligation.t array; remaining : int}
+type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint
+
+module ProgramDecl = struct
+  type t =
+    { prg_name : Id.t
+    ; prg_body : constr
+    ; prg_type : constr
+    ; prg_ctx : UState.t
+    ; prg_univdecl : UState.universe_decl
+    ; prg_obligations : obligations
+    ; prg_deps : Id.t list
+    ; prg_fixkind : fixpoint_kind option
+    ; prg_implicits : Impargs.manual_implicits
+    ; prg_notations : Vernacexpr.decl_notation list
+    ; prg_poly : bool
+    ; prg_scope : locality
+    ; prg_kind : Decls.definition_object_kind
+    ; prg_reduce : constr -> constr
+    ; prg_hook : Hook.t option
+    ; prg_opaque : bool }
+
+  open Obligation
+
+  let make ?(opaque = false) ?hook n ~udecl ~uctx ~impargs ~poly ~scope ~kind b
+      t deps fixkind notations obls reduce =
+    let obls', b =
+      match b with
+      | None ->
+        assert (Int.equal (Array.length obls) 0);
+        let n = Nameops.add_suffix n "_obligation" in
+        ( [| { obl_name = n
+             ; obl_body = None
+             ; obl_location = Loc.tag Evar_kinds.InternalHole
+             ; obl_type = t
+             ; obl_status = (false, Evar_kinds.Expand)
+             ; obl_deps = Int.Set.empty
+             ; obl_tac = None } |]
+        , mkVar n )
+      | Some b ->
+        ( Array.mapi
+            (fun i (n, t, l, o, d, tac) ->
+              { obl_name = n
+              ; obl_body = None
+              ; obl_location = l
+              ; obl_type = t
+              ; obl_status = o
+              ; obl_deps = d
+              ; obl_tac = tac })
+            obls
+        , b )
+    in
+    let ctx = UState.make_flexible_nonalgebraic uctx in
+    { prg_name = n
+    ; prg_body = b
+    ; prg_type = reduce t
+    ; prg_ctx = ctx
+    ; prg_univdecl = udecl
+    ; prg_obligations = {obls = obls'; remaining = Array.length obls'}
+    ; prg_deps = deps
+    ; prg_fixkind = fixkind
+    ; prg_notations = notations
+    ; prg_implicits = impargs
+    ; prg_poly = poly
+    ; prg_scope = scope
+    ; prg_kind = kind
+    ; prg_reduce = reduce
+    ; prg_hook = hook
+    ; prg_opaque = opaque }
+
+  let set_uctx ~uctx prg = {prg with prg_ctx = uctx}
+end
+
+open Obligation
+open ProgramDecl
+
+(* Saving an obligation *)
+
+(* XXX: Is this the right place for this? *)
+let it_mkLambda_or_LetIn_or_clean t ctx =
+  let open Context.Rel.Declaration in
+  let fold t decl =
+    if is_local_assum decl then Term.mkLambda_or_LetIn decl t
+    else if Vars.noccurn 1 t then Vars.subst1 mkProp t
+    else Term.mkLambda_or_LetIn decl t
+  in
+  Context.Rel.fold_inside fold ctx ~init:t
+
+(* XXX: Is this the right place for this? *)
+let decompose_lam_prod c ty =
+  let open Context.Rel.Declaration in
+  let rec aux ctx c ty =
+    match (Constr.kind c, Constr.kind ty) with
+    | LetIn (x, b, t, c), LetIn (x', b', t', ty)
+      when Constr.equal b b' && Constr.equal t t' ->
+      let ctx' = Context.Rel.add (LocalDef (x, b', t')) ctx in
+      aux ctx' c ty
+    | _, LetIn (x', b', t', ty) ->
+      let ctx' = Context.Rel.add (LocalDef (x', b', t')) ctx in
+      aux ctx' (lift 1 c) ty
+    | LetIn (x, b, t, c), _ ->
+      let ctx' = Context.Rel.add (LocalDef (x, b, t)) ctx in
+      aux ctx' c (lift 1 ty)
+    | Lambda (x, b, t), Prod (x', b', t')
+    (* By invariant, must be convertible *) ->
+      let ctx' = Context.Rel.add (LocalAssum (x, b')) ctx in
+      aux ctx' t t'
+    | Cast (c, _, _), _ -> aux ctx c ty
+    | _, _ -> (ctx, c, ty)
+  in
+  aux Context.Rel.empty c ty
+
+(* XXX: What's the relation of this with Abstract.shrink ? *)
+let shrink_body c ty =
+  let ctx, b, ty =
+    match ty with
+    | None ->
+      let ctx, b = Term.decompose_lam_assum c in
+      (ctx, b, None)
+    | Some ty ->
+      let ctx, b, ty = decompose_lam_prod c ty in
+      (ctx, b, Some ty)
+  in
+  let b', ty', n, args =
+    List.fold_left
+      (fun (b, ty, i, args) decl ->
+        if Vars.noccurn 1 b && Option.cata (Vars.noccurn 1) true ty then
+          (Vars.subst1 mkProp b, Option.map (Vars.subst1 mkProp) ty, succ i, args)
+        else
+          let open Context.Rel.Declaration in
+          let args = if is_local_assum decl then mkRel i :: args else args in
+          ( Term.mkLambda_or_LetIn decl b
+          , Option.map (Term.mkProd_or_LetIn decl) ty
+          , succ i
+          , args ))
+      (b, ty, 1, []) ctx
+  in
+  (ctx, b', ty', Array.of_list args)
+
+(***********************************************************************)
+(* Saving an obligation                                                *)
+(***********************************************************************)
+
+let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
+
+let add_hint local prg cst =
+  let locality = if local then Goptions.OptLocal else Goptions.OptExport in
+  Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst)
+
+(* true = hide obligations *)
+let get_hide_obligations =
+  Goptions.declare_bool_option_and_ref
+    ~depr:true
+    ~key:["Hide"; "Obligations"]
+    ~value:false
+
+let declare_obligation prg obl body ty uctx =
+  let body = prg.prg_reduce body in
+  let ty = Option.map prg.prg_reduce ty in
+  match obl.obl_status with
+  | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)})
+  | force, Evar_kinds.Define opaque ->
+    let opaque = (not force) && opaque in
+    let poly = prg.prg_poly in
+    let ctx, body, ty, args =
+      if not poly then shrink_body body ty
+      else ([], body, ty, [||])
+    in
+    let ce = definition_entry ?types:ty ~opaque ~univs:uctx body in
+    (* ppedrot: seems legit to have obligations as local *)
+    let constant =
+      declare_constant ~name:obl.obl_name
+        ~local:ImportNeedQualified
+        ~kind:Decls.(IsProof Property)
+        (DefinitionEntry ce)
+    in
+    if not opaque then
+      add_hint (Locality.make_section_locality None) prg constant;
+    definition_message obl.obl_name;
+    let body =
+      match uctx with
+      | Entries.Polymorphic_entry (_, uctx) ->
+        Some (DefinedObl (constant, Univ.UContext.instance uctx))
+      | Entries.Monomorphic_entry _ ->
+        Some
+          (TermObl
+             (it_mkLambda_or_LetIn_or_clean
+                (mkApp (mkConst constant, args))
+                ctx))
+    in
+    (true, {obl with obl_body = body})
+
+(* Updating the obligation meta-info on close *)
+
+let not_transp_msg =
+  Pp.(
+    str "Obligation should be transparent but was declared opaque."
+    ++ spc ()
+    ++ str "Use 'Defined' instead.")
+
+let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
+let err_not_transp () = pperror not_transp_msg
+
+module ProgMap = Id.Map
+
+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
+
+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_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 "
+        ++ what_for ++ str ":" ++ spc ()
+        ++ prlist_with_sep spc (fun x -> Id.print x) keys
+        ++ str have_string
+        ++ str "unsolved obligations" )
+
+let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
+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 =
+  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
+
+let get_obligation_body expand obl =
+  match obl.obl_body with
+  | None -> None
+  | Some c -> (
+    if expand && snd obl.obl_status == Evar_kinds.Expand then
+      match c with
+      | DefinedObl pc -> Some (Environ.constant_value_in (Global.env ()) pc)
+      | TermObl c -> Some c
+    else
+      match c with DefinedObl pc -> Some (mkConstU pc) | TermObl c -> Some c )
+
+let obl_substitution expand obls deps =
+  Int.Set.fold
+    (fun x acc ->
+      let xobl = obls.(x) in
+      match get_obligation_body expand xobl with
+      | None -> acc
+      | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
+    deps []
+
+let rec intset_to = function
+  | -1 -> Int.Set.empty
+  | n -> Int.Set.add n (intset_to (pred n))
+
+let obligation_substitution expand prg =
+  let obls = prg.prg_obligations.obls in
+  let ints = intset_to (pred (Array.length obls)) in
+  obl_substitution expand obls ints
+
+let hide_obligation () =
+  Coqlib.check_required_library ["Coq"; "Program"; "Tactics"];
+  UnivGen.constr_of_monomorphic_global
+    (Coqlib.lib_ref "program.tactics.obligation")
+
+(* XXX: Is this the right place? *)
+let rec prod_app t n =
+  match
+    Constr.kind
+      (EConstr.Unsafe.to_constr
+         (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t)))
+    (* FIXME *)
+  with
+  | Prod (_, _, b) -> Vars.subst1 n b
+  | LetIn (_, b, t, b') -> prod_app (Vars.subst1 b b') n
+  | _ ->
+    CErrors.user_err ~hdr:"prod_app"
+      Pp.(str "Needed a product, but didn't find one" ++ fnl ())
+
+(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
+let prod_applist t nL = List.fold_left prod_app t nL
+
+let replace_appvars subst =
+  let rec aux c =
+    let f, l = decompose_app c in
+    if isVar f then
+      try
+        let c' = List.map (Constr.map aux) l in
+        let t, b = Id.List.assoc (destVar f) subst in
+        mkApp
+          ( delayed_force hide_obligation
+          , [|prod_applist t c'; Term.applistc b c'|] )
+      with Not_found -> Constr.map aux c
+    else Constr.map aux c
+  in
+  Constr.map aux
+
+let subst_prog subst prg =
+  if get_hide_obligations () then
+    ( replace_appvars subst prg.prg_body
+    , replace_appvars subst (* Termops.refresh_universes *) prg.prg_type )
+  else
+    let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in
+    ( Vars.replace_vars subst' prg.prg_body
+    , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type )
+
+let stm_get_fix_exn = ref (fun _ x -> x)
+
+let declare_definition prg =
+  let varsubst = obligation_substitution true prg in
+  let sigma = Evd.from_ctx prg.prg_ctx in
+  let body, types = subst_prog varsubst prg in
+  let body, types = EConstr.(of_constr body, Some (of_constr types)) in
+  (* All these should be grouped into a struct a some point *)
+  let opaque, poly, udecl, hook =
+    (prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook)
+  in
+  let name, scope, kind, impargs =
+    ( prg.prg_name
+    , prg.prg_scope
+    , Decls.(IsDefinition prg.prg_kind)
+    , prg.prg_implicits )
+  in
+  let fix_exn = !stm_get_fix_exn () in
+  let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
+  (* XXX: This is doing normalization twice *)
+  let kn =
+    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 =
+  match Constr.kind t with
+  | Lambda ({Context.binder_name = Name n'}, _, _) when Id.equal n n' -> acc
+  | Lambda (_, _, b) -> lam_index n b (succ acc)
+  | _ -> raise Not_found
+
+let compute_possible_guardness_evidences n fixbody fixtype =
+  match n with
+  | Some {CAst.loc; v = n} -> [lam_index n fixbody 0]
+  | None ->
+    (* If recursive argument was not given by user, we try all args.
+         An earlier approach was to look only for inductive arguments,
+         but doing it properly involves delta-reduction, and it finally
+         doesn't seem to worth the effort (except for huge mutual
+         fixpoints ?) *)
+    let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (* FIXME *) in
+    let ctx = fst (Term.decompose_prod_n_assum m fixtype) in
+    List.map_i (fun i _ -> i) 0 ctx
+
+let declare_mutual_definition l =
+  let len = List.length l in
+  let first = List.hd l in
+  let defobl x =
+    let oblsubst = obligation_substitution true x in
+    let subs, typ = subst_prog oblsubst x in
+    let env = Global.env () in
+    let sigma = Evd.from_ctx x.prg_ctx in
+    let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in
+    let term =
+      snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs))
+    in
+    let typ =
+      snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ))
+    in
+    let term = EConstr.to_constr sigma term in
+    let typ = EConstr.to_constr sigma typ in
+    let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in
+    let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in
+    (def, oblsubst)
+  in
+  let defs, obls =
+    List.fold_right
+      (fun x (defs, obls) ->
+        let xdef, xobls = defobl x in
+        (xdef :: defs, xobls @ obls))
+      l ([], [])
+  in
+  (*   let fixdefs = List.map reduce_fix fixdefs in *)
+  let fixdefs, fixrs, fixtypes, fixitems =
+    List.fold_right2
+      (fun (d, r, typ, impargs) name (a1, a2, a3, a4) ->
+        ( d :: a1
+        , r :: a2
+        , typ :: a3
+        , Recthm.{name; typ; impargs; args = []} :: a4 ))
+      defs first.prg_deps ([], [], [], [])
+  in
+  let fixkind = Option.get first.prg_fixkind in
+  let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in
+  let rvec = Array.of_list fixrs in
+  let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in
+  let rec_declaration = (Array.map2 Context.make_annot namevec rvec, arrrec, recvec) in
+  let possible_indexes =
+    match fixkind with
+    | IsFixpoint wfl ->
+      Some (List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes)
+    | IsCoFixpoint -> None
+  in
+  (* In the future we will pack all this in a proper record *)
+  let poly, scope, ntns, opaque =
+    (first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque)
+  in
+  let kind =
+    if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint)
+    else Decls.(IsDefinition CoFixpoint)
+  in
+  (* Declare the recursive definitions *)
+  let udecl = UState.default_univ_decl in
+  let kns =
+    declare_mutually_recursive ~scope ~opaque ~kind ~udecl ~ntns
+      ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly
+      ~restrict_ucontext:false fixitems
+  in
+  (* Only for the first constant *)
+  let dref = List.hd kns in
+  Hook.(
+    call ?hook:first.prg_hook {S.uctx = first.prg_ctx; obls; scope; dref});
+  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
+  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
+      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 pm)) prg'.prg_deps
+      in
+      if List.for_all (fun x -> obligations_solved x) progs then
+        let kn = declare_mutual_definition progs in
+        Defined kn
+      else Dependent
+
+let dependencies obls n =
+  let res = ref Int.Set.empty in
+  Array.iteri
+    (fun i obl ->
+      if (not (Int.equal i n)) && Int.Set.mem n obl.obl_deps then
+        res := Int.Set.add i !res)
+    obls;
+  !res
+
+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 _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
+    let ty = entry.proof_entry_type in
+    let body, uctx = inline_private_constants ~uctx env entry in
+    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 = Option.get (State.find name) in
+    let {obls; remaining = rem} = prg.prg_obligations in
+    let obl = obls.(num) in
+    let status =
+      match (obl.obl_status, entry.proof_entry_opaque) with
+      | (_, Evar_kinds.Expand), true -> err_not_transp ()
+      | (true, _), true -> err_not_transp ()
+      | (false, _), true -> Evar_kinds.Define true
+      | (_, Evar_kinds.Define true), false -> Evar_kinds.Define false
+      | (_, status), false -> status
+    in
+    let obl = {obl with obl_status = (false, status)} in
+    let uctx = if prg.prg_poly then uctx else UState.union prg.prg_ctx uctx in
+    let univs = UState.univ_entry ~poly:prg.prg_poly uctx in
+    let defined, obl = declare_obligation prg obl body ty univs in
+    let prg_ctx =
+      if prg.prg_poly then
+        (* Polymorphic *)
+        (* We merge the new universes and constraints of the
+           polymorphic obligation with the existing ones *)
+        UState.union prg.prg_ctx uctx
+      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 *)
+        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
+  | _ ->
+    CErrors.anomaly
+      Pp.(
+        str
+          "[obligation_terminator] close_proof returned more than one proof \
+           term")
+
+(* 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 = Environ.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 ()
+    | _ -> ()
+  in
+  let inst, ctx' =
+    if not prg.prg_poly (* Not polymorphic *) then
+      (* The universe context was declared globally, we continue
+         from the new global environment. *)
+      let ctx =
+        UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
+      in
+      let ctx' = UState.merge_subst ctx (UState.subst ctx') in
+      (Univ.Instance.empty, ctx')
+    else
+      (* We get the right order somehow, but surely it could be enforced in a clearer way. *)
+      let uctx = UState.context ctx' in
+      (Univ.UContext.instance uctx, ctx')
+  in
+  let obl = {obl with obl_body = Some (DefinedObl (cst, inst))} in
+  let () = if transparent then add_hint true prg cst in
+  update_program_decl_on_defined prg obls num obl ~uctx:ctx' rem ~auto
+
+end
+
+(************************************************************************)
+(* Commom constant saving path, for both Qed and Admitted               *)
+(************************************************************************)
+
+(* Support for mutually proved theorems *)
+
+module Proof_ending = struct
+
+  type t =
+    | Regular
+    | End_obligation of Obls.obligation_qed_info
+    | End_derive of { f : Id.t; name : Id.t }
+    | End_equations of
+        { hook : Constant.t list -> Evd.evar_map -> unit
+        ; i : Id.t
+        ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
+        ; sigma : Evd.evar_map
+        }
+
+end
+
+type lemma_possible_guards = int list list
+
+module Info = struct
+
+  type t =
+    { hook : Hook.t option
+    ; proof_ending : Proof_ending.t CEphemeron.key
+    (* This could be improved and the CEphemeron removed *)
+    ; scope : locality
+    ; kind : Decls.logical_kind
+    (* thms and compute guard are specific only to start_lemma_with_initialization + regular terminator *)
+    ; thms : Recthm.t list
+    ; compute_guard : lemma_possible_guards
+    }
+
+  let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Global ImportDefaultBehavior)
+      ?(kind=Decls.(IsProof Lemma)) ?(compute_guard=[]) ?(thms=[]) () =
+    { hook
+    ; compute_guard
+    ; proof_ending = CEphemeron.create proof_ending
+    ; thms
+    ; scope
+    ; kind
+    }
+
+  (* This is used due to a deficiency on the API, should fix *)
+  let add_first_thm ~info ~name ~typ ~impargs =
+    let thms =
+      { Recthm.name
+      ; impargs
+      ; typ = EConstr.Unsafe.to_constr typ
+      ; args = [] } :: info.thms
+    in
+    { info with thms }
+
+end
+
+(* XXX: this should be unified with the code for non-interactive
+   mutuals previously on this file. *)
+module MutualEntry : sig
+
+  val declare_variable
+    : info:Info.t
+    -> uctx:UState.t
+    -> Entries.parameter_entry
+    -> Names.GlobRef.t list
+
+  val declare_mutdef
+    (* Common to all recthms *)
+    : info:Info.t
+    -> uctx:UState.t
+    -> Evd.side_effects proof_entry
+    -> Names.GlobRef.t list
+
+end = struct
+
+  (* XXX: Refactor this with the code in [Declare.declare_mutdef] *)
+  let guess_decreasing env possible_indexes ((body, ctx), eff) =
+    let open Constr in
+    match Constr.kind body with
+    | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
+      let env = Safe_typing.push_private_constants env eff.Evd.seff_private in
+      let indexes = Pretyping.search_guard env possible_indexes fixdecls in
+      (mkFix ((indexes,0),fixdecls), ctx), eff
+    | _ -> (body, ctx), eff
+
+  let select_body i t =
+    let open Constr in
+    match Constr.kind t with
+    | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
+    | CoFix (0,decls) -> mkCoFix (i,decls)
+    | _ ->
+      CErrors.anomaly
+        Pp.(str "Not a proof by induction: " ++
+            Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".")
+
+  let declare_mutdef ~uctx ~info pe i Recthm.{ name; impargs; typ; _} =
+    let { Info.hook; scope; kind; compute_guard; _ } = info in
+    (* if i = 0 , we don't touch the type; this is for compat
+       but not clear it is the right thing to do.
+    *)
+    let pe, ubind =
+      if i > 0 && not (CList.is_empty compute_guard)
+      then Internal.map_entry_type pe ~f:(fun _ -> Some typ), UnivNames.empty_binders
+      else pe, UState.universe_binders uctx
+    in
+    (* We when compute_guard was [] in the previous step we should not
+       substitute the body *)
+    let pe = match compute_guard with
+      | [] -> pe
+      | _ ->
+        Internal.map_entry_body pe
+          ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff)
+    in
+    declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe
+
+  let declare_mutdef ~info ~uctx const =
+    let pe = match info.Info.compute_guard with
+    | [] ->
+      (* Not a recursive statement *)
+      const
+    | possible_indexes ->
+      (* Try all combinations... not optimal *)
+      let env = Global.env() in
+      Internal.map_entry_body const
+        ~f:(guess_decreasing env possible_indexes)
+    in
+    List.map_i (declare_mutdef ~info ~uctx pe) 0 info.Info.thms
+
+  let declare_variable ~info ~uctx pe =
+    let { Info.scope; hook } = info in
+    List.map_i (
+      fun i { Recthm.name; typ; impargs } ->
+        declare_assumption ~name ~scope ~hook ~impargs ~uctx pe
+    ) 0 info.Info.thms
+
+end
+
+(************************************************************************)
+(* Admitting a lemma-like constant                                      *)
+(************************************************************************)
+
+(* Admitted *)
+let get_keep_admitted_vars =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Keep"; "Admitted"; "Variables"]
+    ~value:true
+
+let compute_proof_using_for_admitted proof typ pproofs =
+  if not (get_keep_admitted_vars ()) then None
+  else match get_used_variables proof, pproofs with
+    | Some _ as x, _ -> x
+    | None, pproof :: _ ->
+      let env = Global.env () in
+      let ids_typ = Environ.global_vars_set env typ in
+      (* [pproof] is evar-normalized by [partial_proof]. We don't
+         count variables appearing only in the type of evars. *)
+      let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in
+      Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
+    | _ -> None
+
+let finish_admitted ~info ~uctx pe =
+  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 ->
+    Obls.obligation_admitted_terminator oinfo uctx (List.hd cst)
+  | _ -> ()
+
+let save_lemma_admitted ~proof ~info  =
+  let udecl = get_universe_decl proof in
+  let Proof.{ poly; entry } = Proof.data (get_proof proof) in
+  let typ = match Proofview.initial_goals entry with
+    | [typ] -> snd typ
+    | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.")
+  in
+  let typ = EConstr.Unsafe.to_constr typ in
+  let iproof = get_proof proof in
+  let pproofs = Proof.partial_proof iproof in
+  let sec_vars = compute_proof_using_for_admitted proof typ pproofs in
+  let uctx = get_initial_euctx proof in
+  let univs = UState.check_univ_decl ~poly uctx udecl in
+  finish_admitted ~info ~uctx (sec_vars, (typ, univs), None)
+
+(************************************************************************)
+(* Saving a lemma-like constant                                         *)
+(************************************************************************)
+
+let finish_proved po info =
+  match po with
+  | { entries=[const]; uctx } ->
+    let _r : Names.GlobRef.t list = MutualEntry.declare_mutdef ~info ~uctx const in
+    ()
+  | _ ->
+    CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term")
+
+let finish_derived ~f ~name ~entries =
+  (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *)
+
+  let f_def, lemma_def =
+    match entries with
+    | [_;f_def;lemma_def] ->
+      f_def, lemma_def
+    | _ -> assert false
+  in
+  (* The opacity of [f_def] is adjusted to be [false], as it
+     must. Then [f] is declared in the global environment. *)
+  let f_def = Internal.set_opacity ~opaque:false f_def in
+  let f_kind = Decls.(IsDefinition Definition) in
+  let f_def = DefinitionEntry f_def in
+  let f_kn = declare_constant ~name:f ~kind:f_kind f_def in
+  let f_kn_term = Constr.mkConst f_kn in
+  (* In the type and body of the proof of [suchthat] there can be
+     references to the variable [f]. It needs to be replaced by
+     references to the constant [f] declared above. This substitution
+     performs this precise action. *)
+  let substf c = Vars.replace_vars [f,f_kn_term] c in
+  (* Extracts the type of the proof of [suchthat]. *)
+  let lemma_pretype typ =
+    match typ with
+    | Some t -> Some (substf t)
+    | None -> assert false (* Declare always sets type here. *)
+  in
+  (* The references of [f] are subsituted appropriately. *)
+  let lemma_def = Internal.map_entry_type lemma_def ~f:lemma_pretype in
+  (* The same is done in the body of the proof. *)
+  let lemma_def = Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in
+  let lemma_def = DefinitionEntry lemma_def in
+  let _ : Names.Constant.t = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
+  ()
+
+let finish_proved_equations ~kind ~hook i proof_obj types sigma0 =
+
+  let obls = ref 1 in
+  let sigma, recobls =
+    CList.fold_left2_map (fun sigma (_evar_env, ev, _evi, local_context, _type) entry ->
+        let id =
+          match Evd.evar_ident ev sigma0 with
+          | Some id -> id
+          | None -> let n = !obls in incr obls; Nameops.add_suffix i ("_obligation_" ^ string_of_int n)
+        in
+        let entry, args = Internal.shrink_entry local_context entry in
+        let cst = declare_constant ~name:id ~kind (DefinitionEntry entry) in
+        let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in
+        let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in
+        sigma, cst) sigma0
+      types proof_obj.entries
+  in
+  hook recobls sigma
+
+let finalize_proof proof_obj proof_info =
+  let open Proof_ending in
+  match CEphemeron.default proof_info.Info.proof_ending Regular with
+  | Regular ->
+    finish_proved proof_obj proof_info
+  | End_obligation oinfo ->
+    Obls.obligation_terminator proof_obj.entries proof_obj.uctx oinfo
+  | End_derive { f ; name } ->
+    finish_derived ~f ~name ~entries:proof_obj.entries
+  | End_equations { hook; i; types; sigma } ->
+    finish_proved_equations ~kind:proof_info.Info.kind ~hook i proof_obj types sigma
+
+let err_save_forbidden_in_place_of_qed () =
+  CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode")
+
+let process_idopt_for_save ~idopt info =
+  match idopt with
+  | None -> info
+  | Some { CAst.v = save_name } ->
+    (* Save foo was used; we override the info in the first theorem *)
+    let thms =
+      match info.Info.thms, CEphemeron.default info.Info.proof_ending Proof_ending.Regular with
+      | [ { Recthm.name; _} as decl ], Proof_ending.Regular ->
+        [ { decl with Recthm.name = save_name } ]
+      | _ ->
+        err_save_forbidden_in_place_of_qed ()
+    in { info with Info.thms }
+
+let save_lemma_proved ~proof ~info ~opaque ~idopt =
+  (* Env and sigma are just used for error printing in save_remaining_recthms *)
+  let proof_obj = close_proof ~opaque ~keep_body_ucst_separate:false proof in
+  let proof_info = process_idopt_for_save ~idopt info in
+  finalize_proof proof_obj proof_info
+
+(***********************************************************************)
+(* Special case to close a lemma without forcing a proof               *)
+(***********************************************************************)
+let save_lemma_admitted_delayed ~proof ~info =
+  let { entries; uctx } = proof in
+  if List.length entries <> 1 then
+    CErrors.user_err Pp.(str "Admitted does not support multiple statements");
+  let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
+  let poly = match proof_entry_universes with
+    | Entries.Monomorphic_entry _ -> false
+    | Entries.Polymorphic_entry (_, _) -> true in
+  let typ = match proof_entry_type with
+    | None -> CErrors.user_err Pp.(str "Admitted requires an explicit statement");
+    | Some typ -> typ in
+  let ctx = UState.univ_entry ~poly uctx in
+  let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
+  finish_admitted ~uctx ~info (sec_vars, (typ, ctx), None)
+
+let save_lemma_proved_delayed ~proof ~info ~idopt =
+  (* vio2vo calls this but with invalid info, we have to workaround
+     that to add the name to the info structure *)
+  if CList.is_empty info.Info.thms then
+    let name = get_po_name proof in
+    let info = Info.add_first_thm ~info ~name ~typ:EConstr.mkSet ~impargs:[] in
+    finalize_proof proof info
+  else
+    let info = process_idopt_for_save ~idopt info in
+    finalize_proof proof info
+
+module Proof = struct
+  type nonrec t = t
+  let get_proof = get_proof
+  let get_proof_name = get_proof_name
+  let map_proof = map_proof
+  let map_fold_proof = map_fold_proof
+  let map_fold_proof_endline = map_fold_proof_endline
+  let set_endline_tactic = set_endline_tactic
+  let set_used_variables = set_used_variables
+  let compact = compact_the_proof
+  let update_global_env = update_global_env
+  let get_open_goals = get_open_goals
+end
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 340c035d1d..82b0cff8d9 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -17,9 +17,9 @@ open Entries
    environment. It also updates some accesory tables such as [Nametab]
    (name resolution), [Impargs], and [Notations]. *)
 
-(** We provide two kind of fuctions:
+(** We provide two kind of functions:
 
-  - one go functions, that will register a constant in one go, suited
+  - one-go functions, that will register a constant in one go, suited
    for non-interactive definitions where the term is given.
 
   - two-phase [start/declare] functions which will create an
@@ -29,6 +29,13 @@ open Entries
   Internally, these functions mainly differ in that usually, the first
   case doesn't require setting up the tactic engine.
 
+  Note that the API in this file is still in a state of flux, don't
+  hesitate to contact the maintainers if you have any question.
+
+  Additionally, this file does contain some low-level functions, marked
+  as such; these functions are unstable and should not be used unless you
+  already know what they are doing.
+
  *)
 
 (** [Declare.Proof.t] Construction of constants using interactive proofs. *)
@@ -41,11 +48,6 @@ module Proof : sig
   val get_proof : t -> Proof.t
   val get_proof_name : t -> Names.Id.t
 
-  (** XXX: These 3 are only used in lemmas  *)
-  val get_used_variables : t -> Names.Id.Set.t option
-  val get_universe_decl : t -> UState.universe_decl
-  val get_initial_euctx : t -> UState.t
-
   val map_proof : (Proof.t -> Proof.t) -> t -> t
   val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a
   val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
@@ -97,39 +99,33 @@ val start_dependent_proof
 (** Proof entries represent a proof that has been finished, but still
    not registered with the kernel.
 
-   XXX: Scheduled for removal from public API, don't rely on it *)
-type 'a proof_entry = private {
-  proof_entry_body   : 'a Entries.const_entry_body;
-  (* List of section variables *)
-  proof_entry_secctx : Id.Set.t option;
-  (* State id on which the completion of type checking is reported *)
-  proof_entry_feedback : Stateid.t option;
-  proof_entry_type        : Constr.types option;
-  proof_entry_universes   : Entries.universes_entry;
-  proof_entry_opaque      : bool;
-  proof_entry_inline_code : bool;
-}
-
-(** XXX: Scheduled for removal from public API, don't rely on it *)
-type proof_object = private
-  { name : Names.Id.t
-  (** name of the proof *)
-  ; entries : Evd.side_effects proof_entry list
-  (** list of the proof terms (in a form suitable for definitions). *)
-  ; uctx: UState.t
-  (** universe state *)
-  }
+   XXX: This is an internal, low-level API and could become scheduled
+   for removal from the public API, use higher-level declare APIs
+   instead *)
+type 'a proof_entry
+
+(** XXX: This is an internal, low-level API and could become scheduled
+   for removal from the public API, use higher-level declare APIs
+   instead *)
+type proof_object
+
+(** Used by the STM only to store info, should go away *)
+val get_po_name : proof_object -> Id.t
 
 val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t -> proof_object
 
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
-(** XXX: Scheduled for removal from public API, don't rely on it *)
+(** XXX: This is an internal, low-level API and could become scheduled
+   for removal from the public API, use higher-level declare APIs
+   instead *)
 type variable_declaration =
   | SectionLocalDef of Evd.side_effects proof_entry
   | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; }
 
-(** XXX: Scheduled for removal from public API, don't rely on it *)
+(** XXX: This is an internal, low-level API and could become scheduled
+   for removal from the public API, use higher-level declare APIs
+   instead *)
 type 'a constant_entry =
   | DefinitionEntry of 'a proof_entry
   | ParameterEntry of parameter_entry
@@ -144,7 +140,9 @@ val declare_variable
 (** Declaration of global constructions
    i.e. Definition/Theorem/Axiom/Parameter/...
 
-   XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
+   XXX: This is an internal, low-level API and could become scheduled
+   for removal from the public API, use higher-level declare APIs
+   instead *)
 val definition_entry
   : ?fix_exn:Future.fix_exn
   -> ?opaque:bool
@@ -160,7 +158,7 @@ val definition_entry
   -> constr
   -> Evd.side_effects proof_entry
 
-type import_status = ImportDefaultBehavior | ImportNeedQualified
+type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeedQualified
 
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
@@ -169,7 +167,9 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified
   internal specify if the constant has been created by the kernel or by the
   user, and in the former case, if its errors should be silent
 
-  XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
+  XXX: This is an internal, low-level API and could become scheduled
+  for removal from the public API, use higher-level declare APIs
+  instead *)
 val declare_constant
   :  ?local:import_status
   -> name:Id.t
@@ -177,17 +177,6 @@ val declare_constant
   -> Evd.side_effects constant_entry
   -> Constant.t
 
-(** [inline_private_constants ~sideff ~uctx env ce] will inline the
-   constants in [ce]'s body and return the body plus the updated
-   [UState.t].
-
-   XXX: Scheduled for removal from public API, don't rely on it *)
-val inline_private_constants
-  :  uctx:UState.t
-  -> Environ.env
-  -> Evd.side_effects proof_entry
-  -> Constr.t * UState.t
-
 (** Declaration messages *)
 
 (** XXX: Scheduled for removal from public API, do not use *)
@@ -201,13 +190,6 @@ val check_exists : Id.t -> unit
 
 module Internal : sig
 
-  val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry
-  val map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entry
-  (* Overriding opacity is indeed really hacky *)
-  val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry
-
-  val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list
-
   type constant_obj
 
   val objConstant : constant_obj Libobject.Dyn.tag
@@ -233,6 +215,7 @@ val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output
     Returns [false] if an unsafe tactic has been used. *)
 val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool
 
+(** Semantics of this function is a bit dubious, use with care *)
 val build_by_tactic
   :  ?side_eff:bool
   -> Environ.env
@@ -260,7 +243,7 @@ val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env
   environment and empty evar_map. *)
 val get_current_context : Proof.t -> Evd.evar_map * Environ.env
 
-(** Temporarily re-exported for 3rd party code; don't use  *)
+(** XXX: Temporarily re-exported for 3rd party code; don't use  *)
 val build_constant_by_tactic :
   name:Names.Id.t ->
   ?opaque:opacity_flag ->
@@ -270,11 +253,12 @@ val build_constant_by_tactic :
   EConstr.types ->
   unit Proofview.tactic ->
   Evd.side_effects proof_entry * bool * UState.t
+[@@ocaml.deprecated "This function is deprecated, used newer API in declare"]
 
 val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
 [@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"]
 
-type locality = Discharge | Global of import_status
+type locality = Locality.locality = Discharge | Global of import_status
 
 (** Declaration hooks *)
 module Hook : sig
@@ -303,7 +287,9 @@ module Hook : sig
   val call : ?hook:t -> S.t -> unit
 end
 
-(** Declare an interactively-defined constant *)
+(** XXX: This is an internal, low-level API and could become scheduled
+    for removal from the public API, use higher-level declare APIs
+    instead *)
 val declare_entry
   :  name:Id.t
   -> scope:locality
@@ -361,6 +347,8 @@ module Recthm : sig
     }
 end
 
+type lemma_possible_guards = int list list
+
 val declare_mutually_recursive
   : opaque:bool
   -> scope:locality
@@ -370,13 +358,14 @@ val declare_mutually_recursive
   -> udecl:UState.universe_decl
   -> ntns:Vernacexpr.decl_notation list
   -> rec_declaration:Constr.rec_declaration
-  -> possible_indexes:int list list option
+  -> possible_indexes:lemma_possible_guards option
   -> ?restrict_ucontext:bool
   (** XXX: restrict_ucontext should be always true, this seems like a
      bug in obligations, so this parameter should go away *)
   -> Recthm.t list
   -> Names.GlobRef.t list
 
+(** Prepare API, to be removed once we provide the corresponding 1-step API *)
 val prepare_obligation
   :  ?opaque:bool
   -> ?inline:bool
@@ -397,3 +386,214 @@ val prepare_parameter
 
 (* Compat: will remove *)
 exception AlreadyDeclared of (string option * Names.Id.t)
+
+module Obls : sig
+
+type 'a obligation_body = DefinedObl of 'a | TermObl of constr
+
+module Obligation : sig
+  type t = private
+    { obl_name : Id.t
+    ; obl_type : types
+    ; obl_location : Evar_kinds.t Loc.located
+    ; obl_body : pconstant obligation_body option
+    ; obl_status : bool * Evar_kinds.obligation_definition_status
+    ; obl_deps : Int.Set.t
+    ; obl_tac : unit Proofview.tactic option }
+
+  val set_type : typ:Constr.types -> t -> t
+  val set_body : body:pconstant obligation_body -> t -> t
+end
+
+type obligations = {obls : Obligation.t array; remaining : int}
+type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint
+
+(* Information about a single [Program {Definition,Lemma,..}] declaration *)
+module ProgramDecl : sig
+  type t = private
+    { prg_name : Id.t
+    ; prg_body : constr
+    ; prg_type : constr
+    ; prg_ctx : UState.t
+    ; prg_univdecl : UState.universe_decl
+    ; prg_obligations : obligations
+    ; prg_deps : Id.t list
+    ; prg_fixkind : fixpoint_kind option
+    ; prg_implicits : Impargs.manual_implicits
+    ; prg_notations : Vernacexpr.decl_notation list
+    ; prg_poly : bool
+    ; prg_scope : locality
+    ; prg_kind : Decls.definition_object_kind
+    ; prg_reduce : constr -> constr
+    ; prg_hook : Hook.t option
+    ; prg_opaque : bool }
+
+  val make :
+       ?opaque:bool
+    -> ?hook:Hook.t
+    -> Names.Id.t
+    -> udecl:UState.universe_decl
+    -> uctx:UState.t
+    -> impargs:Impargs.manual_implicits
+    -> poly:bool
+    -> scope:locality
+    -> kind:Decls.definition_object_kind
+    -> Constr.constr option
+    -> Constr.types
+    -> 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
+    -> (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
+  -> Constr.types
+  -> Constr.types option
+  -> Entries.universes_entry
+  -> bool * Obligation.t
+
+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
+
+(** Resolution status of a program *)
+type progress =
+  | Remain of int  (** n obligations remaining *)
+  | Dependent  (** Dependent on other definitions *)
+  | 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 : obligation_resolver}
+
+(** [update_obls prg obls n progress] What does this do? *)
+val update_obls :
+  ProgramDecl.t -> Obligation.t array -> int -> progress
+
+(** Check obligations are properly solved before closing the
+   [what_for] section / module *)
+val check_solved_obligations : what_for:Pp.t -> unit
+
+(** { 2 Util }  *)
+
+val obl_substitution :
+     bool
+  -> Obligation.t array
+  -> Int.Set.t
+  -> (Id.t * (Constr.types * Constr.types)) list
+
+val dependencies : Obligation.t array -> int -> Int.Set.t
+val err_not_transp : unit -> 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
+ * is not available here, so we provide a side channel to get it *)
+val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) ref
+
+end
+
+(** Creating high-level proofs with an associated constant *)
+module Proof_ending : sig
+
+  type t =
+    | Regular
+    | End_obligation of Obls.obligation_qed_info
+    | End_derive of { f : Id.t; name : Id.t }
+    | End_equations of
+        { hook : Constant.t list -> Evd.evar_map -> unit
+        ; i : Id.t
+        ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
+        ; sigma : Evd.evar_map
+        }
+
+end
+
+module Info : sig
+  type t
+  val make
+    :  ?hook: Hook.t
+    (** Callback to be executed at the end of the proof *)
+    -> ?proof_ending : Proof_ending.t
+    (** Info for special constants *)
+    -> ?scope : locality
+    (** locality  *)
+    -> ?kind:Decls.logical_kind
+    (** Theorem, etc... *)
+    -> ?compute_guard:lemma_possible_guards
+    -> ?thms:Recthm.t list
+    (** Both of those are internal, used by the upper layers but will
+       become handled natively here in the future *)
+    -> unit
+    -> t
+
+  (* Internal; used to initialize non-mutual proofs *)
+  val add_first_thm :
+    info:t
+    -> name:Id.t
+    -> typ:EConstr.t
+    -> impargs:Impargs.manual_implicits
+    -> t
+end
+
+val save_lemma_proved
+  : proof:Proof.t
+  -> info:Info.t
+  -> opaque:opacity_flag
+  -> idopt:Names.lident option
+  -> unit
+
+val save_lemma_admitted :
+     proof:Proof.t
+  -> info:Info.t
+  -> unit
+
+(** Special cases for delayed proofs, in this case we must provide the
+   proof information so the proof won't be forced. *)
+val save_lemma_admitted_delayed :
+     proof:proof_object
+  -> info:Info.t
+  -> unit
+
+val save_lemma_proved_delayed
+  : proof:proof_object
+  -> info:Info.t
+  -> idopt:Names.lident option
+  -> unit
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
deleted file mode 100644
index 9ea54f5d8f..0000000000
--- a/vernac/declareObl.ml
+++ /dev/null
@@ -1,578 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Util
-open Names
-open Environ
-open Context
-open Constr
-open Vars
-open Entries
-
-type 'a obligation_body = DefinedObl of 'a | TermObl of constr
-
-module Obligation = struct
-  type t =
-    { obl_name : Id.t
-    ; obl_type : types
-    ; obl_location : Evar_kinds.t Loc.located
-    ; obl_body : pconstant obligation_body option
-    ; obl_status : bool * Evar_kinds.obligation_definition_status
-    ; obl_deps : Int.Set.t
-    ; obl_tac : unit Proofview.tactic option }
-
-  let set_type ~typ obl = { obl with obl_type = typ }
-  let set_body ~body obl = { obl with obl_body = Some body }
-
-end
-
-type obligations =
-  { obls : Obligation.t array
-  ; remaining : int }
-
-type fixpoint_kind =
-  | IsFixpoint of lident option list
-  | IsCoFixpoint
-
-module ProgramDecl = struct
-
-  type t =
-    { prg_name : Id.t
-    ; prg_body : constr
-    ; prg_type : constr
-    ; prg_ctx : UState.t
-    ; prg_univdecl : UState.universe_decl
-    ; prg_obligations : obligations
-    ; prg_deps : Id.t list
-    ; prg_fixkind : fixpoint_kind option
-    ; prg_implicits : Impargs.manual_implicits
-    ; prg_notations : Vernacexpr.decl_notation list
-    ; prg_poly : bool
-    ; prg_scope : Declare.locality
-    ; prg_kind : Decls.definition_object_kind
-    ; prg_reduce : constr -> constr
-    ; prg_hook : Declare.Hook.t option
-    ; prg_opaque : bool
-    }
-
-  open Obligation
-
-  let make ?(opaque = false) ?hook n ~udecl ~uctx ~impargs
-      ~poly ~scope ~kind b t deps fixkind notations obls reduce =
-    let obls', b =
-      match b with
-      | None ->
-        assert(Int.equal (Array.length obls) 0);
-        let n = Nameops.add_suffix n "_obligation" in
-        [| { obl_name = n; obl_body = None;
-             obl_location = Loc.tag Evar_kinds.InternalHole; obl_type = t;
-             obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty;
-             obl_tac = None } |],
-        mkVar n
-      | Some b ->
-        Array.mapi
-          (fun i (n, t, l, o, d, tac) ->
-             { obl_name = n ; obl_body = None;
-               obl_location = l; obl_type = t; obl_status = o;
-               obl_deps = d; obl_tac = tac })
-          obls, b
-    in
-    let ctx = UState.make_flexible_nonalgebraic uctx in
-    { prg_name = n
-    ; prg_body = b
-    ; prg_type = reduce t
-    ; prg_ctx = ctx
-    ; prg_univdecl = udecl
-    ; prg_obligations = { obls = obls' ; remaining = Array.length obls' }
-    ; prg_deps = deps
-    ; prg_fixkind = fixkind
-    ; prg_notations = notations
-    ; prg_implicits = impargs
-    ; prg_poly = poly
-    ; prg_scope = scope
-    ; prg_kind = kind
-    ; prg_reduce = reduce
-    ; prg_hook = hook
-    ; prg_opaque = opaque
-    }
-
-  let set_uctx ~uctx prg = {prg with prg_ctx = uctx}
-end
-
-open Obligation
-open ProgramDecl
-
-(* Saving an obligation *)
-
-(* XXX: Is this the right place for this? *)
-let it_mkLambda_or_LetIn_or_clean t ctx =
-  let open Context.Rel.Declaration in
-  let fold t decl =
-    if is_local_assum decl then Term.mkLambda_or_LetIn decl t
-    else if noccurn 1 t then subst1 mkProp t
-    else Term.mkLambda_or_LetIn decl t
-  in
-  Context.Rel.fold_inside fold ctx ~init:t
-
-(* XXX: Is this the right place for this? *)
-let decompose_lam_prod c ty =
-  let open Context.Rel.Declaration in
-  let rec aux ctx c ty =
-    match (Constr.kind c, Constr.kind ty) with
-    | LetIn (x, b, t, c), LetIn (x', b', t', ty)
-      when Constr.equal b b' && Constr.equal t t' ->
-      let ctx' = Context.Rel.add (LocalDef (x, b', t')) ctx in
-      aux ctx' c ty
-    | _, LetIn (x', b', t', ty) ->
-      let ctx' = Context.Rel.add (LocalDef (x', b', t')) ctx in
-      aux ctx' (lift 1 c) ty
-    | LetIn (x, b, t, c), _ ->
-      let ctx' = Context.Rel.add (LocalDef (x, b, t)) ctx in
-      aux ctx' c (lift 1 ty)
-    | Lambda (x, b, t), Prod (x', b', t')
-    (* By invariant, must be convertible *) ->
-      let ctx' = Context.Rel.add (LocalAssum (x, b')) ctx in
-      aux ctx' t t'
-    | Cast (c, _, _), _ -> aux ctx c ty
-    | _, _ -> (ctx, c, ty)
-  in
-  aux Context.Rel.empty c ty
-
-(* XXX: What's the relation of this with Abstract.shrink ? *)
-let shrink_body c ty =
-  let ctx, b, ty =
-    match ty with
-    | None ->
-      let ctx, b = Term.decompose_lam_assum c in
-      (ctx, b, None)
-    | Some ty ->
-      let ctx, b, ty = decompose_lam_prod c ty in
-      (ctx, b, Some ty)
-  in
-  let b', ty', n, args =
-    List.fold_left
-      (fun (b, ty, i, args) decl ->
-        if noccurn 1 b && Option.cata (noccurn 1) true ty then
-          (subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args)
-        else
-          let open Context.Rel.Declaration in
-          let args = if is_local_assum decl then mkRel i :: args else args in
-          ( Term.mkLambda_or_LetIn decl b
-          , Option.map (Term.mkProd_or_LetIn decl) ty
-          , succ i
-          , args ) )
-      (b, ty, 1, []) ctx
-  in
-  (ctx, b', ty', Array.of_list args)
-
-(***********************************************************************)
-(* Saving an obligation                                                *)
-(***********************************************************************)
-
-let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
-
-let add_hint local prg cst =
-  let locality = if local then Goptions.OptLocal else Goptions.OptExport in
-  Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst)
-
-(* true = hide obligations *)
-let get_hide_obligations =
-  Goptions.declare_bool_option_and_ref
-    ~depr:true
-    ~key:["Hide"; "Obligations"]
-    ~value:false
-
-let declare_obligation prg obl body ty uctx =
-  let body = prg.prg_reduce body in
-  let ty = Option.map prg.prg_reduce ty in
-  match obl.obl_status with
-  | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)})
-  | force, Evar_kinds.Define opaque ->
-    let opaque = (not force) && opaque in
-    let poly = prg.prg_poly in
-    let ctx, body, ty, args =
-      if not poly then shrink_body body ty
-      else ([], body, ty, [||])
-    in
-    let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in
-
-    (* ppedrot: seems legit to have obligations as local *)
-    let constant =
-      Declare.declare_constant ~name:obl.obl_name
-        ~local:Declare.ImportNeedQualified ~kind:Decls.(IsProof Property)
-        (Declare.DefinitionEntry ce)
-    in
-    if not opaque then
-      add_hint (Locality.make_section_locality None) prg constant;
-    Declare.definition_message obl.obl_name;
-    let body =
-      match uctx with
-      | Polymorphic_entry (_, uctx) ->
-        Some (DefinedObl (constant, Univ.UContext.instance uctx))
-      | Monomorphic_entry _ ->
-        Some
-          (TermObl
-             (it_mkLambda_or_LetIn_or_clean
-                (mkApp (mkConst constant, args))
-                ctx))
-    in
-    (true, {obl with obl_body = body})
-
-(* Updating the obligation meta-info on close *)
-
-let not_transp_msg =
-  Pp.(
-    str "Obligation should be transparent but was declared opaque."
-    ++ spc ()
-    ++ str "Use 'Defined' instead.")
-
-let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
-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"
-
-(* 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
-
-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
-    CErrors.user_err ~hdr:"Program"
-      Pp.(
-        str "Unsolved obligations when closing "
-        ++ 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 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
-
-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")
-
-type progress = Remain of int | Dependent | Defined of GlobRef.t
-
-let get_obligation_body expand obl =
-  match obl.obl_body with
-  | None -> None
-  | Some c -> (
-    if expand && snd obl.obl_status == Evar_kinds.Expand then
-      match c with
-      | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc)
-      | TermObl c -> Some c
-    else
-      match c with DefinedObl pc -> Some (mkConstU pc) | TermObl c -> Some c )
-
-let obl_substitution expand obls deps =
-  Int.Set.fold
-    (fun x acc ->
-      let xobl = obls.(x) in
-      match get_obligation_body expand xobl with
-      | None -> acc
-      | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc )
-    deps []
-
-let rec intset_to = function
-  | -1 -> Int.Set.empty
-  | n -> Int.Set.add n (intset_to (pred n))
-
-let obligation_substitution expand prg =
-  let obls = prg.prg_obligations.obls in
-  let ints = intset_to (pred (Array.length obls)) in
-  obl_substitution expand obls ints
-
-let hide_obligation () =
-  Coqlib.check_required_library ["Coq"; "Program"; "Tactics"];
-  UnivGen.constr_of_monomorphic_global
-    (Coqlib.lib_ref "program.tactics.obligation")
-
-(* XXX: Is this the right place? *)
-let rec prod_app t n =
-  match
-    Constr.kind
-      (EConstr.Unsafe.to_constr
-         (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t)))
-    (* FIXME *)
-  with
-  | Prod (_, _, b) -> subst1 n b
-  | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
-  | _ ->
-    CErrors.user_err ~hdr:"prod_app"
-      Pp.(str "Needed a product, but didn't find one" ++ fnl ())
-
-(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
-let prod_applist t nL = List.fold_left prod_app t nL
-
-let replace_appvars subst =
-  let rec aux c =
-    let f, l = decompose_app c in
-    if isVar f then
-      try
-        let c' = List.map (Constr.map aux) l in
-        let t, b = Id.List.assoc (destVar f) subst in
-        mkApp
-          ( delayed_force hide_obligation
-          , [|prod_applist t c'; Term.applistc b c'|] )
-      with Not_found -> Constr.map aux c
-    else Constr.map aux c
-  in
-  Constr.map aux
-
-let subst_prog subst prg =
-  if get_hide_obligations () then
-    ( replace_appvars subst prg.prg_body
-    , replace_appvars subst (* Termops.refresh_universes *) prg.prg_type )
-  else
-    let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in
-    ( Vars.replace_vars subst' prg.prg_body
-    , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type )
-
-let get_fix_exn, stm_get_fix_exn = Hook.make ()
-
-let declare_definition prg =
-  let varsubst = obligation_substitution true prg in
-  let sigma = Evd.from_ctx prg.prg_ctx in
-  let body, types = subst_prog varsubst prg in
-  let body, types = EConstr.(of_constr body, Some (of_constr types)) in
-  (* All these should be grouped into a struct a some point *)
-  let opaque, poly, udecl, hook = prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook in
-  let name, scope, kind, impargs = prg.prg_name, prg.prg_scope, Decls.(IsDefinition prg.prg_kind), prg.prg_implicits in
-  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
-  kn
-
-let rec lam_index n t acc =
-  match Constr.kind t with
-  | Lambda ({binder_name=Name n'}, _, _) when Id.equal n n' -> acc
-  | Lambda (_, _, b) -> lam_index n b (succ acc)
-  | _ -> raise Not_found
-
-let compute_possible_guardness_evidences n fixbody fixtype =
-  match n with
-  | Some {CAst.loc; v = n} -> [lam_index n fixbody 0]
-  | None ->
-    (* If recursive argument was not given by user, we try all args.
-         An earlier approach was to look only for inductive arguments,
-         but doing it properly involves delta-reduction, and it finally
-         doesn't seem to worth the effort (except for huge mutual
-         fixpoints ?) *)
-    let m =
-      Termops.nb_prod Evd.empty (EConstr.of_constr fixtype)
-      (* FIXME *)
-    in
-    let ctx = fst (Term.decompose_prod_n_assum m fixtype) in
-    List.map_i (fun i _ -> i) 0 ctx
-
-let declare_mutual_definition l =
-  let len = List.length l in
-  let first = List.hd l in
-  let defobl x =
-    let oblsubst = obligation_substitution true x in
-    let subs, typ = subst_prog oblsubst x in
-    let env = Global.env () in
-    let sigma = Evd.from_ctx x.prg_ctx in
-    let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in
-    let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
-    let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
-    let term = EConstr.to_constr sigma term in
-    let typ = EConstr.to_constr sigma typ in
-    let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in
-    let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in
-    def, oblsubst
-  in
-  let defs, obls =
-    List.fold_right (fun x (defs, obls) ->
-        let xdef, xobls = defobl x in
-        (xdef :: defs, xobls @ obls)) l ([], [])
-  in
-  (*   let fixdefs = List.map reduce_fix fixdefs in *)
-  let fixdefs, fixrs, fixtypes, fixitems =
-    List.fold_right2 (fun (d,r,typ,impargs) name (a1,a2,a3,a4) ->
-        d :: a1, r :: a2, typ :: a3,
-        Declare.Recthm.{ name; typ; impargs; args = [] } :: a4
-      ) defs first.prg_deps ([],[],[],[])
-  in
-  let fixkind = Option.get first.prg_fixkind in
-  let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in
-  let rvec = Array.of_list fixrs in
-  let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in
-  let rec_declaration = (Array.map2 make_annot namevec rvec, arrrec, recvec) in
-  let possible_indexes =
-    match fixkind with
-    | IsFixpoint wfl ->
-      Some (List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes)
-    | IsCoFixpoint -> None
-  in
-  (* In the future we will pack all this in a proper record *)
-  let poly, scope, ntns, opaque = first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque in
-  let kind = if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) else Decls.(IsDefinition CoFixpoint) in
-  (* Declare the recursive definitions *)
-  let udecl = UState.default_univ_decl in
-  let kns =
-    Declare.declare_mutually_recursive ~scope ~opaque ~kind
-      ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly
-      ~restrict_ucontext:false fixitems
-  in
-  (* 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;
-  dref
-
-let update_obls prg obls rem =
-  let prg_obligations = { obls; remaining = rem } in
-  let prg' = {prg with prg_obligations} in
-  progmap_replace prg';
-  obligations_message rem;
-  if rem > 0 then Remain rem
-  else
-    match prg'.prg_deps with
-    | [] ->
-      let kn = declare_definition prg' in
-      progmap_remove prg';
-      Defined kn
-    | l ->
-      let progs =
-        List.map
-          (fun x -> CEphemeron.get (ProgMap.find x !from_prg))
-          prg'.prg_deps
-      in
-      if List.for_all (fun x -> obligations_solved x) progs then
-        let kn = declare_mutual_definition progs in
-        Defined kn
-      else Dependent
-
-let dependencies obls n =
-  let res = ref Int.Set.empty in
-  Array.iteri
-    (fun i obl ->
-      if (not (Int.equal i n)) && Int.Set.mem n obl.obl_deps then
-        res := Int.Set.add i !res )
-    obls;
-  !res
-
-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 } =
-  match entries with
-  | [entry] ->
-    let env = Global.env () in
-    let ty = entry.Declare.proof_entry_type in
-    let body, uctx = Declare.inline_private_constants ~uctx env entry in
-    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 { obls; remaining=rem } = prg.prg_obligations in
-    let obl = obls.(num) in
-    let status =
-      match obl.obl_status, entry.Declare.proof_entry_opaque with
-      | (_, Evar_kinds.Expand), true -> err_not_transp ()
-      | (true, _), true -> err_not_transp ()
-      | (false, _), true -> Evar_kinds.Define true
-      | (_, Evar_kinds.Define true), false ->
-        Evar_kinds.Define false
-      | (_, status), false -> status
-    in
-    let obl = { obl with obl_status = false, status } in
-    let uctx =
-      if prg.prg_poly then uctx
-      else UState.union prg.prg_ctx uctx
-    in
-    let univs = UState.univ_entry ~poly:prg.prg_poly uctx in
-    let (defined, obl) = declare_obligation prg obl body ty univs in
-    let prg_ctx =
-      if prg.prg_poly then (* Polymorphic *)
-        (* We merge the new universes and constraints of the
-           polymorphic obligation with the existing ones *)
-        UState.union prg.prg_ctx uctx
-      else
-        (* 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
-    in
-    update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto
-  | _ ->
-    CErrors.anomaly
-      Pp.(
-        str
-          "[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
-  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 ()
-    | _ -> ()
-  in
-  let inst, ctx' =
-    if not prg.prg_poly (* Not polymorphic *) then
-      (* The universe context was declared globally, we continue
-         from the new global environment. *)
-      let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
-      let ctx' = UState.merge_subst ctx (UState.subst ctx') in
-      Univ.Instance.empty, ctx'
-    else
-      (* We get the right order somehow, but surely it could be enforced in a clearer way. *)
-      let uctx = UState.context ctx' in
-      Univ.UContext.instance uctx, ctx'
-  in
-  let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
-  let () = if transparent then add_hint true prg cst in
-  update_program_decl_on_defined prg obls num obl ~uctx:ctx' rem ~auto
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
deleted file mode 100644
index 03f0a57bcb..0000000000
--- a/vernac/declareObl.mli
+++ /dev/null
@@ -1,164 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-open Constr
-
-type 'a obligation_body = DefinedObl of 'a | TermObl of constr
-
-module Obligation : sig
-
-  type t = private
-    { obl_name : Id.t
-    ; obl_type : types
-    ; obl_location : Evar_kinds.t Loc.located
-    ; obl_body : pconstant obligation_body option
-    ; obl_status : bool * Evar_kinds.obligation_definition_status
-    ; obl_deps : Int.Set.t
-    ; obl_tac : unit Proofview.tactic option }
-
-  val set_type : typ:Constr.types -> t -> t
-  val set_body : body:pconstant obligation_body -> t -> t
-
-end
-
-type obligations =
-  { obls : Obligation.t array
-  ; remaining : int }
-
-type fixpoint_kind =
-  | IsFixpoint of lident option list
-  | IsCoFixpoint
-
-(* Information about a single [Program {Definition,Lemma,..}] declaration *)
-module ProgramDecl : sig
-
-  type t = private
-    { prg_name : Id.t
-    ; prg_body : constr
-    ; prg_type : constr
-    ; prg_ctx : UState.t
-    ; prg_univdecl : UState.universe_decl
-    ; prg_obligations : obligations
-    ; prg_deps : Id.t list
-    ; prg_fixkind : fixpoint_kind option
-    ; prg_implicits : Impargs.manual_implicits
-    ; prg_notations : Vernacexpr.decl_notation list
-    ; prg_poly : bool
-    ; prg_scope : Declare.locality
-    ; prg_kind : Decls.definition_object_kind
-    ; prg_reduce : constr -> constr
-    ; prg_hook : Declare.Hook.t option
-    ; prg_opaque : bool
-    }
-
-  val make :
-    ?opaque:bool
-    -> ?hook:Declare.Hook.t
-    -> Names.Id.t
-    -> udecl:UState.universe_decl
-    -> uctx:UState.t
-    -> impargs:Impargs.manual_implicits
-    -> poly:bool
-    -> scope:Declare.locality
-    -> kind:Decls.definition_object_kind
-    -> Constr.constr option
-    -> Constr.types
-    -> 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
-    -> (Constr.constr -> Constr.constr)
-    -> t
-
-  val set_uctx : uctx:UState.t -> t -> t
-end
-
-val declare_obligation :
-     ProgramDecl.t
-  -> Obligation.t
-  -> Constr.types
-  -> 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
-
-val declare_definition : ProgramDecl.t -> Names.GlobRef.t
-
-(** Resolution status of a program *)
-type progress =
-  | Remain of int
-  (** n obligations remaining *)
-  | Dependent
-  (** Dependent on other definitions *)
-  | Defined of GlobRef.t
-  (** Defined as id *)
-
-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
-  -> unit
-(** [obligation_hook] part 2 of saving an obligation, non-interactive mode *)
-
-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
-
-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
-
-val obl_substitution :
-     bool
-  -> Obligation.t array
-  -> Int.Set.t
-  -> (ProgMap.key * (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
- * is not available here, so we provide a side channel to get it *)
-val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 838496c595..10d63ff2ff 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -12,7 +12,6 @@
    file command.ml, Aug 2009 *)
 
 open Util
-open Names
 
 module NamedDecl = Context.Named.Declaration
 
@@ -21,44 +20,8 @@ module NamedDecl = Context.Named.Declaration
 
 type lemma_possible_guards = int list list
 
-module Proof_ending = struct
-
-  type t =
-    | Regular
-    | End_obligation of DeclareObl.obligation_qed_info
-    | End_derive of { f : Id.t; name : Id.t }
-    | End_equations of
-        { hook : Constant.t list -> Evd.evar_map -> unit
-        ; i : Id.t
-        ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
-        ; sigma : Evd.evar_map
-        }
-
-end
-
-module Info = struct
-
-  type t =
-    { hook : Declare.Hook.t option
-    ; proof_ending : Proof_ending.t CEphemeron.key
-    (* This could be improved and the CEphemeron removed *)
-    ; scope : Declare.locality
-    ; kind : Decls.logical_kind
-    (* thms and compute guard are specific only to start_lemma_with_initialization + regular terminator *)
-    ; thms : Declare.Recthm.t list
-    ; compute_guard : lemma_possible_guards
-    }
-
-  let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Declare.Global Declare.ImportDefaultBehavior)
-      ?(kind=Decls.(IsProof Lemma)) () =
-    { hook
-    ; compute_guard = []
-    ; proof_ending = CEphemeron.create proof_ending
-    ; thms = []
-    ; scope
-    ; kind
-    }
-end
+module Proof_ending = Declare.Proof_ending
+module Info = Declare.Info
 
 (* Proofs with a save constant function *)
 type t =
@@ -96,15 +59,6 @@ let initialize_named_context_for_proof () =
       let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in
       Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
 
-let add_first_thm ~info ~name ~typ ~impargs =
-  let thms =
-    { Declare.Recthm.name
-    ; impargs
-    ; typ = EConstr.Unsafe.to_constr typ
-    ; args = [] } :: info.Info.thms
-  in
-  { info with Info.thms }
-
 (* Starting a goal *)
 let start_lemma ~name ~poly
     ?(udecl=UState.default_univ_decl)
@@ -114,7 +68,7 @@ let start_lemma ~name ~poly
   let sign = initialize_named_context_for_proof () in
   let goals = [ Global.env_of_context sign , c ] in
   let proof = Declare.start_proof sigma ~name ~udecl ~poly goals in
-  let info = add_first_thm ~info ~name ~typ:c ~impargs in
+  let info = Declare.Info.add_first_thm ~info ~name ~typ:c ~impargs in
   { proof; info }
 
 (* Note that proofs opened by start_dependent lemma cannot be closed
@@ -162,276 +116,15 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
   match thms with
   | [] -> CErrors.anomaly (Pp.str "No proof to start.")
   | { Declare.Recthm.name; typ; impargs; _} :: thms ->
-    let info =
-      Info.{ hook
-           ; compute_guard
-           ; proof_ending = CEphemeron.create Proof_ending.Regular
-           ; thms
-           ; scope
-           ; kind
-           } in
+    let info = Info.make ?hook ~scope ~kind ~compute_guard ~thms () in
     (* start_lemma has the responsibility to add (name, impargs, typ)
        to thms, once Info.t is more refined this won't be necessary *)
     let lemma = start_lemma ~name ~impargs ~poly ~udecl ~info sigma (EConstr.of_constr typ) in
     pf_map (Declare.Proof.map_proof (fun p ->
         pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)) lemma
 
-(************************************************************************)
-(* Commom constant saving path, for both Qed and Admitted               *)
-(************************************************************************)
-
-(* Support for mutually proved theorems *)
-
-(* XXX: Most of this does belong to Declare, due to proof_entry manip *)
-module MutualEntry : sig
-
-  val declare_variable
-    : info:Info.t
-    -> uctx:UState.t
-    -> Entries.parameter_entry
-    -> Names.GlobRef.t list
-
-  val declare_mutdef
-    (* Common to all recthms *)
-    : info:Info.t
-    -> uctx:UState.t
-    -> Evd.side_effects Declare.proof_entry
-    -> Names.GlobRef.t list
-
-end = struct
-
-  (* XXX: Refactor this with the code in [Declare.declare_mutdef] *)
-  let guess_decreasing env possible_indexes ((body, ctx), eff) =
-    let open Constr in
-    match Constr.kind body with
-    | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
-      let env = Safe_typing.push_private_constants env eff.Evd.seff_private in
-      let indexes = Pretyping.search_guard env possible_indexes fixdecls in
-      (mkFix ((indexes,0),fixdecls), ctx), eff
-    | _ -> (body, ctx), eff
-
-  let select_body i t =
-    let open Constr in
-    match Constr.kind t with
-    | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
-    | CoFix (0,decls) -> mkCoFix (i,decls)
-    | _ ->
-      CErrors.anomaly
-        Pp.(str "Not a proof by induction: " ++
-            Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".")
-
-  let declare_mutdef ~uctx ~info pe i Declare.Recthm.{ name; impargs; typ; _} =
-    let { Info.hook; scope; kind; compute_guard; _ } = info in
-    (* if i = 0 , we don't touch the type; this is for compat
-       but not clear it is the right thing to do.
-    *)
-    let pe, ubind =
-      if i > 0 && not (CList.is_empty compute_guard)
-      then Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ), UnivNames.empty_binders
-      else pe, UState.universe_binders uctx
-    in
-    (* We when compute_guard was [] in the previous step we should not
-       substitute the body *)
-    let pe = match compute_guard with
-      | [] -> pe
-      | _ ->
-        Declare.Internal.map_entry_body pe
-          ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff)
-    in
-    Declare.declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe
-
-  let declare_mutdef ~info ~uctx const =
-    let pe = match info.Info.compute_guard with
-    | [] ->
-      (* Not a recursive statement *)
-      const
-    | possible_indexes ->
-      (* Try all combinations... not optimal *)
-      let env = Global.env() in
-      Declare.Internal.map_entry_body const
-        ~f:(guess_decreasing env possible_indexes)
-    in
-    List.map_i (declare_mutdef ~info ~uctx pe) 0 info.Info.thms
-
-  let declare_variable ~info ~uctx pe =
-    let { Info.scope; hook } = info in
-    List.map_i (
-      fun i { Declare.Recthm.name; typ; impargs } ->
-        Declare.declare_assumption ~name ~scope ~hook ~impargs ~uctx pe
-    ) 0 info.Info.thms
-
-end
-
-(************************************************************************)
-(* Admitting a lemma-like constant                                      *)
-(************************************************************************)
-
-(* Admitted *)
-let get_keep_admitted_vars =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Keep"; "Admitted"; "Variables"]
-    ~value:true
-
-let compute_proof_using_for_admitted proof typ pproofs =
-  if not (get_keep_admitted_vars ()) then None
-  else match Declare.Proof.get_used_variables proof, pproofs with
-    | Some _ as x, _ -> x
-    | None, pproof :: _ ->
-      let env = Global.env () in
-      let ids_typ = Environ.global_vars_set env typ in
-      (* [pproof] is evar-normalized by [partial_proof]. We don't
-         count variables appearing only in the type of evars. *)
-      let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in
-      Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
-    | _ -> 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 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
-    | [typ] -> snd typ
-    | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.")
-  in
-  let typ = EConstr.Unsafe.to_constr typ in
-  let proof = Declare.Proof.get_proof lemma.proof in
-  let pproofs = Proof.partial_proof proof in
-  let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in
-  let uctx = Declare.Proof.get_initial_euctx lemma.proof in
-  let univs = UState.check_univ_decl ~poly uctx udecl in
-  finish_admitted ~info:lemma.info ~uctx (sec_vars, (typ, univs), None)
-
-(************************************************************************)
-(* Saving a lemma-like constant                                         *)
-(************************************************************************)
-
-let finish_proved po info =
-  let open Declare in
-  match po with
-  | { entries=[const]; uctx } ->
-    let _r : Names.GlobRef.t list = MutualEntry.declare_mutdef ~info ~uctx const in
-    ()
-  | _ ->
-    CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term")
-
-let finish_derived ~f ~name ~entries =
-  (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *)
-
-  let f_def, lemma_def =
-    match entries with
-    | [_;f_def;lemma_def] ->
-      f_def, lemma_def
-    | _ -> assert false
-  in
-  (* The opacity of [f_def] is adjusted to be [false], as it
-     must. Then [f] is declared in the global environment. *)
-  let f_def = Declare.Internal.set_opacity ~opaque:false f_def in
-  let f_kind = Decls.(IsDefinition Definition) in
-  let f_def = Declare.DefinitionEntry f_def in
-  let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in
-  let f_kn_term = Constr.mkConst f_kn in
-  (* In the type and body of the proof of [suchthat] there can be
-     references to the variable [f]. It needs to be replaced by
-     references to the constant [f] declared above. This substitution
-     performs this precise action. *)
-  let substf c = Vars.replace_vars [f,f_kn_term] c in
-  (* Extracts the type of the proof of [suchthat]. *)
-  let lemma_pretype typ =
-    match typ with
-    | Some t -> Some (substf t)
-    | None -> assert false (* Declare always sets type here. *)
-  in
-  (* The references of [f] are subsituted appropriately. *)
-  let lemma_def = Declare.Internal.map_entry_type lemma_def ~f:lemma_pretype in
-  (* The same is done in the body of the proof. *)
-  let lemma_def = Declare.Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in
-  let lemma_def = Declare.DefinitionEntry lemma_def in
-  let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
-  ()
-
-let finish_proved_equations ~kind ~hook i proof_obj types sigma0 =
-
-  let obls = ref 1 in
-  let sigma, recobls =
-    CList.fold_left2_map (fun sigma (_evar_env, ev, _evi, local_context, _type) entry ->
-        let id =
-          match Evd.evar_ident ev sigma0 with
-          | Some id -> id
-          | None -> let n = !obls in incr obls; Nameops.add_suffix i ("_obligation_" ^ string_of_int n)
-        in
-        let entry, args = Declare.Internal.shrink_entry local_context entry in
-        let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in
-        let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in
-        let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in
-        sigma, cst) sigma0
-      types proof_obj.Declare.entries
-  in
-  hook recobls sigma
-
-let finalize_proof proof_obj proof_info =
-  let open Declare in
-  let open Proof_ending in
-  match CEphemeron.default proof_info.Info.proof_ending Regular with
-  | Regular ->
-    finish_proved proof_obj proof_info
-  | End_obligation oinfo ->
-    DeclareObl.obligation_terminator proof_obj.entries proof_obj.uctx oinfo
-  | End_derive { f ; name } ->
-    finish_derived ~f ~name ~entries:proof_obj.entries
-  | End_equations { hook; i; types; sigma } ->
-    finish_proved_equations ~kind:proof_info.Info.kind ~hook i proof_obj types sigma
-
-let err_save_forbidden_in_place_of_qed () =
-  CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode")
-
-let process_idopt_for_save ~idopt info =
-  match idopt with
-  | None -> info
-  | Some { CAst.v = save_name } ->
-    (* Save foo was used; we override the info in the first theorem *)
-    let thms =
-      match info.Info.thms, CEphemeron.default info.Info.proof_ending Proof_ending.Regular with
-      | [ { Declare.Recthm.name; _} as decl ], Proof_ending.Regular ->
-        [ { decl with Declare.Recthm.name = save_name } ]
-      | _ ->
-        err_save_forbidden_in_place_of_qed ()
-    in { info with Info.thms }
+let save_lemma_admitted ~lemma =
+  Declare.save_lemma_admitted ~proof:lemma.proof ~info:lemma.info
 
 let save_lemma_proved ~lemma ~opaque ~idopt =
-  (* Env and sigma are just used for error printing in save_remaining_recthms *)
-  let proof_obj = Declare.close_proof ~opaque ~keep_body_ucst_separate:false lemma.proof in
-  let proof_info = process_idopt_for_save ~idopt lemma.info in
-  finalize_proof proof_obj proof_info
-
-(***********************************************************************)
-(* Special case to close a lemma without forcing a proof               *)
-(***********************************************************************)
-let save_lemma_admitted_delayed ~proof ~info =
-  let open Declare in
-  let { entries; uctx } = proof in
-  if List.length entries <> 1 then
-    CErrors.user_err Pp.(str "Admitted does not support multiple statements");
-  let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
-  let poly = match proof_entry_universes with
-    | Entries.Monomorphic_entry _ -> false
-    | Entries.Polymorphic_entry (_, _) -> true in
-  let typ = match proof_entry_type with
-    | None -> CErrors.user_err Pp.(str "Admitted requires an explicit statement");
-    | Some typ -> typ in
-  let ctx = UState.univ_entry ~poly uctx in
-  let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
-  finish_admitted ~uctx ~info (sec_vars, (typ, ctx), None)
-
-let save_lemma_proved_delayed ~proof ~info ~idopt =
-  (* vio2vo calls this but with invalid info, we have to workaround
-     that to add the name to the info structure *)
-  if CList.is_empty info.Info.thms then
-    let info = add_first_thm ~info ~name:proof.Declare.name ~typ:EConstr.mkSet ~impargs:[] in
-    finalize_proof proof info
-  else
-    let info = process_idopt_for_save ~idopt info in
-    finalize_proof proof info
+  Declare.save_lemma_proved ~proof:lemma.proof ~info:lemma.info ~opaque ~idopt
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index b1462f1ce5..4787a940da 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -28,39 +28,8 @@ val pf_fold : (Declare.Proof.t -> 'a) -> t -> 'a
 val by : unit Proofview.tactic -> t -> t * bool
 (** [by tac l] apply a tactic to [l] *)
 
-(** Creating high-level proofs with an associated constant *)
-module Proof_ending : sig
-
-  type t =
-    | Regular
-    | End_obligation of DeclareObl.obligation_qed_info
-    | End_derive of { f : Id.t; name : Id.t }
-    | End_equations of
-        { hook : Constant.t list -> Evd.evar_map -> unit
-        ; i : Id.t
-        ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
-        ; sigma : Evd.evar_map
-        }
-
-end
-
-module Info : sig
-
-  type t
-
-  val make
-    :  ?hook: Declare.Hook.t
-    (** Callback to be executed at the end of the proof *)
-    -> ?proof_ending : Proof_ending.t
-    (** Info for special constants *)
-    -> ?scope : Declare.locality
-    (** locality  *)
-    -> ?kind:Decls.logical_kind
-    (** Theorem, etc... *)
-    -> unit
-    -> t
-
-end
+module Proof_ending = Declare.Proof_ending
+module Info = Declare.Info
 
 (** Starts the proof of a constant *)
 val start_lemma
@@ -99,6 +68,7 @@ val start_lemma_with_initialization
 (** {4 Saving proofs} *)
 
 val save_lemma_admitted : lemma:t -> unit
+
 val save_lemma_proved
   :  lemma:t
   -> opaque:Declare.opacity_flag
@@ -110,12 +80,3 @@ module Internal : sig
   val get_info : t -> Info.t
   (** Only needed due to the Declare compatibility layer. *)
 end
-
-(** Special cases for delayed proofs, in this case we must provide the
-   proof information so the proof won't be forced. *)
-val save_lemma_admitted_delayed : proof:Declare.proof_object -> info:Info.t -> unit
-val save_lemma_proved_delayed
-  :  proof:Declare.proof_object
-  -> info:Info.t
-  -> idopt:Names.lident option
-  -> unit
diff --git a/vernac/locality.ml b/vernac/locality.ml
index f62eed5e41..3953e54f52 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -10,9 +10,12 @@
 
 (** * Managing locality *)
 
+type import_status = ImportDefaultBehavior | ImportNeedQualified
+type locality = Discharge | Global of import_status
+
 let importability_of_bool = function
-  | true -> Declare.ImportNeedQualified
-  | false -> Declare.ImportDefaultBehavior
+  | true -> ImportNeedQualified
+  | false -> ImportDefaultBehavior
 
 (** Positioning locality for commands supporting discharging and export
      outside of modules *)
@@ -34,15 +37,14 @@ let warn_local_declaration =
         strbrk "available without qualification when imported.")
 
 let enforce_locality_exp locality_flag discharge =
-  let open Declare in
   let open Vernacexpr in
   match locality_flag, discharge with
   | Some b, NoDischarge -> Global (importability_of_bool b)
-  | None, NoDischarge -> Global Declare.ImportDefaultBehavior
+  | None, NoDischarge -> Global ImportDefaultBehavior
   | None, DoDischarge when not (Global.sections_are_opened ()) ->
      (* If a Let/Variable is defined outside a section, then we consider it as a local definition *)
      warn_local_declaration ();
-     Global Declare.ImportNeedQualified
+     Global ImportNeedQualified
   | None, DoDischarge -> Discharge
   | Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case")
   | Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case")
diff --git a/vernac/locality.mli b/vernac/locality.mli
index bf65579efd..81da895568 100644
--- a/vernac/locality.mli
+++ b/vernac/locality.mli
@@ -10,6 +10,9 @@
 
 (** * Managing locality *)
 
+type import_status = ImportDefaultBehavior | ImportNeedQualified
+type locality = Discharge | Global of import_status
+
 (** * Positioning locality for commands supporting discharging and export
     outside of modules *)
 
@@ -20,7 +23,7 @@
 
 val make_locality : bool option -> bool
 val make_non_locality : bool option -> bool
-val enforce_locality_exp : bool option -> Vernacexpr.discharge -> Declare.locality
+val enforce_locality_exp : bool option -> Vernacexpr.discharge -> locality
 val enforce_locality : bool option -> bool
 
 (** For commands whose default is to not discharge but to export:
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 30ebf425d0..5fdee9f2d4 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -9,39 +9,57 @@
 (************************************************************************)
 
 open Printf
-
 open Names
 open Pp
-open CErrors
 open Util
 
 (* For the records fields, opens should go away one these types are private *)
-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)
+open Declare.Obls
+open Declare.Obls.Obligation
+open Declare.Obls.ProgramDecl
 
 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)
 
 let subst_deps expand obls deps t =
-  let osubst = DeclareObl.obl_substitution expand obls deps in
+  let osubst = Declare.Obls.obl_substitution expand obls deps in
     (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
 
 let subst_deps_obl obls obl =
@@ -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
@@ -173,9 +141,11 @@ let rec solve_obligation prg num tac =
   let evd = Evd.from_ctx prg.prg_ctx in
   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 proof_ending =
+    Declare.Proof_ending.End_obligation
+      {Declare.Obls.name = prg.prg_name; num; auto}
+  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 +154,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 +192,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 +208,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 +267,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 ".");
-    let cst = DeclareObl.declare_definition prg in
+    Flags.if_verbose (msg_generating_obl name) obls;
+    let cst = Declare.Obls.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 +371,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)
+  Declare.Obls.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..102a17b216 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -84,7 +84,7 @@ val add_definition :
   -> ?hook:Declare.Hook.t
   -> ?opaque:bool
   -> RetrieveObl.obligation_info
-  -> DeclareObl.progress
+  -> Declare.Obls.progress
 
 (* XXX: unify with MutualEntry *)
 
@@ -102,7 +102,7 @@ val add_mutual_definitions :
   -> ?hook:Declare.Hook.t
   -> ?opaque:bool
   -> Vernacexpr.decl_notation list
-  -> DeclareObl.fixpoint_kind
+  -> Declare.Obls.fixpoint_kind
   -> unit
 
 (** Implementation of the [Obligation] command *)
@@ -117,7 +117,7 @@ val next_obligation :
 
 (** Implementation of the [Solve Obligation] command *)
 val solve_obligations :
-  Names.Id.t option -> unit Proofview.tactic option -> DeclareObl.progress
+  Names.Id.t option -> unit Proofview.tactic option -> Declare.Obls.progress
 
 val solve_all_obligations : unit Proofview.tactic option -> unit
 
@@ -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/pfedit.ml b/vernac/pfedit.ml
index e6c66ee503..150311ffaa 100644
--- a/vernac/pfedit.ml
+++ b/vernac/pfedit.ml
@@ -15,5 +15,5 @@ let build_by_tactic ?side_eff env ~uctx ~poly ~typ tac =
   b, t, safe, uctx
 [@@ocaml.deprecated "Use [Proof.build_by_tactic]"]
 
-let build_constant_by_tactic = Declare.build_constant_by_tactic
+let build_constant_by_tactic = Declare.build_constant_by_tactic [@ocaml.warning "-3"]
 [@@ocaml.deprecated "Use [Proof.build_constant_by_tactic]"]
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/vernac.mllib b/vernac/vernac.mllib
index a09a473afe..1cad052bce 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -16,7 +16,6 @@ Metasyntax
 DeclareUniv
 RetrieveObl
 Declare
-DeclareObl
 ComHints
 Canonical
 RecLemmas
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 35e625859b..106fed124e 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
+  Declare.Obls.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
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 19d41c4770..7d25e6b852 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -225,9 +225,9 @@ let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option =
   let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
   let () = match pe with
     | Admitted ->
-      Lemmas.save_lemma_admitted_delayed ~proof ~info
+      Declare.save_lemma_admitted_delayed ~proof ~info
     | Proved (_,idopt) ->
-      Lemmas.save_lemma_proved_delayed ~proof ~info ~idopt in
+      Declare.save_lemma_proved_delayed ~proof ~info ~idopt in
   stack
 
 let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } =