[declare] Grand unification of the proof save path.

We complete some arduous refactoring in order to bring all the
internals and code of constant / proof saving into the same module.

In particular, this PR moves the remaining parts of proof saving from
`Lemmas` to `Declare`.

The reduction in exposed internals is considerable; in particular, we
remove the export of the internals of `proof_entry` and `proof_object`
[used in delayed proofs], which will allow us to start to address many
issues with the current setup, such as #10363 .

There are still some TODOs, that will be addressed in subsequent PRs:

- Remove `declare_constant` in favor of higher-level APIs
- Then, remove access to `proof_entry` entirely
- Refactor current very verbose handling of proof info.
- Remove compat modules / API.
- Rework handling of delayed proofs [this may be hard due to state and the STM]
- Reify Hook API for the case where it acts as a continuation [that is to say, declaring constants from the Hook]

List of remaining offenders for `proof_entry` / `declare_constant` in
the codebase:

- File "vernac/comHints.ml"
- File "vernac/indschemes.ml"
- File "vernac/comProgramFixpoint.ml"
- File "vernac/comAssumption.ml"
- File "vernac/record.ml"
- File "plugins/ltac/leminv.ml"
- File "plugins/setoid_ring/newring.ml"
- File "plugins/funind/recdef.ml"
- File "plugins/funind/gen_principle.ml"

9 files changed, 462 insertions, 437 deletions

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 177a76e64b..04f08e488b 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -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
diff --git a/vernac/declare.ml b/vernac/declare.ml
index a34b069f2f..c291890dce 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -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
@@ -1703,3 +1688,332 @@ let obligation_admitted_terminator {name; num; auto} ctx' dref =
   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 2c4a801f9a..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
@@ -169,7 +167,9 @@ type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeed
   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
@@ -190,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
@@ -260,6 +253,7 @@ 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"]
@@ -293,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
@@ -351,6 +347,8 @@ module Recthm : sig
     }
 end
 
+type lemma_possible_guards = int list list
+
 val declare_mutually_recursive
   : opaque:bool
   -> scope:locality
@@ -360,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
@@ -505,17 +504,6 @@ type obligation_resolver =
 
 type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver}
 
-(** [obligation_terminator] part 2 of saving an obligation, proof mode *)
-val obligation_terminator :
-    Evd.side_effects proof_entry list
-  -> UState.t
-  -> obligation_qed_info
-  -> unit
-
-(** [obligation_admitted_terminator] part 2 of saving an obligation, non-interactive mode *)
-val obligation_admitted_terminator :
-  obligation_qed_info -> UState.t -> GlobRef.t -> unit
-
 (** [update_obls prg obls n progress] What does this do? *)
 val update_obls :
   ProgramDecl.t -> Obligation.t array -> int -> progress
@@ -541,3 +529,71 @@ val err_not_transp : unit -> unit
 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/lemmas.ml b/vernac/lemmas.ml
index 15c4b44581..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 Declare.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 = 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,280 +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 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 ->
-    Declare.Obls.obligation_admitted_terminator oinfo uctx (List.hd cst)
-  | _ -> ()
-
-let save_lemma_admitted ~(lemma : t) =
-  let udecl = Declare.Proof.get_universe_decl lemma.proof in
-  let Proof.{ poly; entry } = Proof.data (Declare.Proof.get_proof lemma.proof) in
-  let typ = match Proofview.initial_goals entry with
-    | [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 ->
-    Declare.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
-      | [ { 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 edc5f33e34..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 Declare.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: 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/obligations.ml b/vernac/obligations.ml
index b84e20f6d0..5fdee9f2d4 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -141,7 +141,10 @@ 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 (Declare.Obls.{name = prg.prg_name; num; auto}) 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
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/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 } =