[declare] Move proof information to declare.

At this point the record in lemmas was just a stub; next commit will
stop exposing the internals of mutual information, and pave the way
for the refactoring of `Info.t` handling in the Declare interface.

19 files changed, 314 insertions, 396 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 21e2afe6a9..973c6f8e7c 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 _ : Declare.Obls.progress =
+  let _ : Declare.progress =
     Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls
   in ()
 
@@ -358,7 +358,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
   let sigma = Evd.reset_future_goals sigma in
   let kind = Decls.(IsDefinition Instance) in
   let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in
-  let info = Lemmas.Info.make ~hook ~kind () in
+  let info = Declare.Info.make ~hook ~kind () in
   (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails!
      This is due to a bug in proof_global :( *)
   let termtype = Evarutil.nf_evar sigma termtype in
@@ -374,15 +374,15 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
           Tactics.New.reduce_after_refine;
         ]
       in
-      let lemma, _ = Lemmas.by init_refine lemma in
+      let lemma, _ = Declare.by init_refine lemma in
       lemma
     | None ->
-      let lemma, _ = Lemmas.by (Tactics.auto_intros_tac ids) lemma in
+      let lemma, _ = Declare.by (Tactics.auto_intros_tac ids) lemma in
       lemma
   in
   match tac with
   | Some tac ->
-    let lemma, _ = Lemmas.by tac lemma in
+    let lemma, _ = Declare.by tac lemma in
     lemma
   | None ->
     lemma
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 1b6deb3b28..07695b5bef 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -36,7 +36,7 @@ val new_instance_interactive
   -> ?hook:(GlobRef.t -> unit)
   -> Vernacexpr.hint_info_expr
   -> (bool * constr_expr) option
-  -> Id.t * Lemmas.t
+  -> Id.t * Declare.Proof.t
 
 val new_instance
   :  ?global:bool (** Not global by default. *)
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index d56917271c..a791e67bb1 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 ~body ~types evd in
-  let _ : Declare.Obls.progress =
+  let _ : Declare.progress =
     Obligations.add_definition
       ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls
   in ()
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 0b75e7f410..2995df4a66 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -322,7 +322,7 @@ let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) =
   let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl in
   fixl, ntns, fix, List.map compute_possible_guardness_evidences info
 
-let do_fixpoint_interactive ~scope ~poly l : Lemmas.t =
+let do_fixpoint_interactive ~scope ~poly l : Declare.Proof.t =
   let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
   let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in
   lemma
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 62a9d10bae..486d0156f9 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -16,13 +16,13 @@ open Vernacexpr
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint_interactive :
-  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t
+  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t
 
 val do_fixpoint :
   scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit
 
 val do_cofixpoint_interactive :
-  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t
+  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t
 
 val do_cofixpoint :
   scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit
diff --git a/vernac/declare.ml b/vernac/declare.ml
index e039cbc771..b2f46c2a83 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -18,6 +18,106 @@ module NamedDecl = Context.Named.Declaration
 
 type opacity_flag = Vernacexpr.opacity_flag = Opaque | Transparent
 
+(* Hooks naturally belong here as they apply to both definitions and lemmas *)
+module Hook = struct
+  module S = struct
+    type t =
+      { uctx : UState.t
+      (** [ustate]: universe constraints obtained when the term was closed *)
+      ; obls : (Names.Id.t * Constr.t) list
+      (** [(n1,t1),...(nm,tm)]: association list between obligation
+          name and the corresponding defined term (might be a constant,
+          but also an arbitrary term in the Expand case of obligations) *)
+      ; scope : Locality.locality
+      (**  [locality]: Locality of the original declaration *)
+      ; dref : Names.GlobRef.t
+      (** [ref]: identifier of the original declaration *)
+      }
+  end
+
+  type t = (S.t -> unit) CEphemeron.key
+
+  let make hook = CEphemeron.create hook
+
+  let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook
+
+end
+
+type progress = Remain of int | Dependent | Defined of GlobRef.t
+
+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}
+
+module Proof_ending = struct
+
+  type t =
+    | Regular
+    | End_obligation of 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 Recthm = struct
+  type t =
+    { name : Names.Id.t
+    (** Name of theorem *)
+    ; typ : Constr.t
+    (** Type of theorem  *)
+    ; args : Names.Name.t list
+    (** Names to pre-introduce  *)
+    ; impargs : Impargs.manual_implicits
+    (** Explicitily declared implicit arguments  *)
+    }
+end
+
+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.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=Locality.Global Locality.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
+
 type t =
   { endline_tactic : Genarg.glob_generic_argument option
   ; section_vars : Id.Set.t option
@@ -26,6 +126,7 @@ type t =
   (** Initial universe declarations *)
   ; initial_euctx : UState.t
   (** The initial universe context (for the statement) *)
+  ; info : Info.t
   }
 
 (*** Proof Global manipulation ***)
@@ -35,6 +136,7 @@ let get_proof_name ps = (Proof.data ps.proof).Proof.name
 
 let get_initial_euctx ps = ps.initial_euctx
 
+let fold_proof f p = f p.proof
 let map_proof f p = { p with proof = f p.proof }
 let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res
 
@@ -73,7 +175,7 @@ let initialize_named_context_for_proof () =
    conclusion). The proof is started in the evar map [sigma] (which
    can typically contain universe constraints), and with universe
    bindings [udecl]. *)
-let start_proof_core ~name ~udecl ~poly ?(sign=initialize_named_context_for_proof ()) sigma typ =
+let start_proof_core ~name ~udecl ~poly ?(impargs=[]) ?(sign=initialize_named_context_for_proof ()) ~info sigma typ =
   (* In ?sign, we remove the bodies of variables in the named context
      marked "opaque", this is a hack tho, see #10446, and
      build_constant_by_tactic uses a different method that would break
@@ -81,16 +183,18 @@ let start_proof_core ~name ~udecl ~poly ?(sign=initialize_named_context_for_proo
   let goals = [Global.env_of_context sign, typ] in
   let proof = Proof.start ~name ~poly sigma goals in
   let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+  let info = Info.add_first_thm ~name ~typ ~impargs ~info in
   { proof
   ; endline_tactic = None
   ; section_vars = None
   ; udecl
   ; initial_euctx
+  ; info
   }
 
 let start_proof = start_proof_core ?sign:None
 
-let start_dependent_proof ~name ~udecl ~poly goals =
+let start_dependent_proof ~name ~udecl ~poly ~info goals =
   let proof = Proof.dependent_start ~name ~poly goals in
   let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
   { proof
@@ -98,6 +202,7 @@ let start_dependent_proof ~name ~udecl ~poly goals =
   ; section_vars = None
   ; udecl
   ; initial_euctx
+  ; info
   }
 
 let get_used_variables pf = pf.section_vars
@@ -774,7 +879,8 @@ let by tac = map_fold_proof (Proof.solve (Goal_select.SelectNth 1) None tac)
 
 let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ tac =
   let evd = Evd.from_ctx uctx in
-  let pf = start_proof_core ~name ~poly ~sign ~udecl:UState.default_univ_decl evd typ in
+  let info = Info.make () in
+  let pf = start_proof_core ~name ~poly ~sign ~udecl:UState.default_univ_decl ~impargs:[] ~info evd typ in
   let pf, status = by tac pf in
   let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in
   match entries with
@@ -887,31 +993,6 @@ let declare_universe_context = DeclareUctx.declare_universe_context
 
 type locality = Locality.locality = | Discharge | Global of import_status
 
-(* Hooks naturally belong here as they apply to both definitions and lemmas *)
-module Hook = struct
-  module S = struct
-    type t =
-      { uctx : UState.t
-      (** [ustate]: universe constraints obtained when the term was closed *)
-      ; obls : (Names.Id.t * Constr.t) list
-      (** [(n1,t1),...(nm,tm)]: association list between obligation
-          name and the corresponding defined term (might be a constant,
-          but also an arbitrary term in the Expand case of obligations) *)
-      ; scope : locality
-      (**  [locality]: Locality of the original declaration *)
-      ; dref : Names.GlobRef.t
-      (** [ref]: identifier of the original declaration *)
-      }
-  end
-
-  type t = (S.t -> unit) CEphemeron.key
-
-  let make hook = CEphemeron.create hook
-
-  let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook
-
-end
-
 (* Locality stuff *)
 let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
   let should_suggest =
@@ -952,19 +1033,6 @@ let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
     let vars = Vars.universes_of_constr (List.hd fixdecls) in
     vars, fixdecls, None
 
-module Recthm = struct
-  type t =
-    { name : Names.Id.t
-    (** Name of theorem *)
-    ; typ : Constr.t
-    (** Type of theorem  *)
-    ; args : Names.Name.t list
-    (** Names to pre-introduce  *)
-    ; impargs : Impargs.manual_implicits
-    (** Explicitily declared implicit arguments  *)
-    }
-end
-
 let declare_mutually_recursive_core ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
   let vars, fixdecls, indexes =
     mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
@@ -1373,8 +1441,6 @@ let obligations_message rem =
     (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
@@ -1614,14 +1680,6 @@ let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto =
   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] ->
@@ -1711,58 +1769,6 @@ end
 
 (* 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
@@ -1876,7 +1882,7 @@ let finish_admitted ~info ~uctx pe =
     Obls.obligation_admitted_terminator oinfo uctx (List.hd cst)
   | _ -> ()
 
-let save_lemma_admitted ~proof ~info  =
+let save_lemma_admitted ~proof =
   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
@@ -1889,7 +1895,7 @@ let save_lemma_admitted ~proof ~info  =
   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)
+  finish_admitted ~info:proof.info ~uctx (sec_vars, (typ, univs), None)
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
@@ -1985,10 +1991,10 @@ let process_idopt_for_save ~idopt info =
         err_save_forbidden_in_place_of_qed ()
     in { info with Info.thms }
 
-let save_lemma_proved ~proof ~info ~opaque ~idopt =
+let save_lemma_proved ~proof ~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
+  let proof_info = process_idopt_for_save ~idopt proof.info in
   finalize_proof proof_obj proof_info
 
 (***********************************************************************)
@@ -2022,14 +2028,16 @@ let save_lemma_proved_delayed ~proof ~info ~idopt =
 
 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 get = get_proof
+  let get_name = get_proof_name
+  let fold ~f = fold_proof f
+  let map ~f = map_proof f
+  let map_fold ~f = map_fold_proof f
+  let map_fold_endline ~f = map_fold_proof_endline f
   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
+  let get_info { info } = info
 end
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 4023b082b3..ef35628de2 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -38,6 +38,98 @@ open Entries
 
  *)
 
+(** Declaration hooks *)
+module Hook : sig
+  type t
+
+  (** Hooks allow users of the API to perform arbitrary actions at
+     proof/definition saving time. For example, to register a constant
+     as a Coercion, perform some cleanup, update the search database,
+     etc...  *)
+  module S : sig
+    type t =
+      { uctx : UState.t
+      (** [ustate]: universe constraints obtained when the term was closed *)
+      ; obls : (Id.t * Constr.t) list
+      (** [(n1,t1),...(nm,tm)]: association list between obligation
+          name and the corresponding defined term (might be a constant,
+          but also an arbitrary term in the Expand case of obligations) *)
+      ; scope : Locality.locality
+      (** [scope]: Locality of the original declaration *)
+      ; dref : GlobRef.t
+      (** [dref]: identifier of the original declaration *)
+      }
+  end
+
+  val make : (S.t -> unit) -> t
+  val call : ?hook:t -> S.t -> unit
+end
+
+(** 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}
+
+(** Creating high-level proofs with an associated constant *)
+module Proof_ending : sig
+
+  type t =
+    | Regular
+    | End_obligation of 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 Recthm : sig
+  type t =
+    { name : Id.t
+    (** Name of theorem *)
+    ; typ : Constr.t
+    (** Type of theorem  *)
+    ; args : Name.t list
+    (** Names to pre-introduce  *)
+    ; impargs : Impargs.manual_implicits
+    (** Explicitily declared implicit arguments  *)
+    }
+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
+    (** 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
+
+end
+
 (** [Declare.Proof.t] Construction of constants using interactive proofs. *)
 module Proof : sig
 
@@ -45,12 +137,13 @@ module Proof : sig
 
   (** XXX: These are internal and will go away from publis API once
      lemmas is merged here *)
-  val get_proof : t -> Proof.t
-  val get_proof_name : t -> Names.Id.t
+  val get : t -> Proof.t
+  val get_name : t -> Names.Id.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
+  val fold : f:(Proof.t -> 'a) -> t -> 'a
+  val map : f:(Proof.t -> Proof.t) -> t -> t
+  val map_fold : f:(Proof.t -> Proof.t * 'a) -> t -> t * 'a
+  val map_fold_endline : f:(unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
 
   (** Sets the tactic to be used when a tactic line is closed with [...] *)
   val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
@@ -69,6 +162,8 @@ module Proof : sig
 
   val get_open_goals : t -> int
 
+  (* Internal, don't use *)
+  val get_info : t -> Info.t
 end
 
 type opacity_flag = Vernacexpr.opacity_flag = Opaque | Transparent
@@ -83,6 +178,8 @@ val start_proof
   :  name:Names.Id.t
   -> udecl:UState.universe_decl
   -> poly:bool
+  -> ?impargs:Impargs.manual_implicits
+  -> info:Info.t
   -> Evd.evar_map
   -> EConstr.t
   -> Proof.t
@@ -93,6 +190,7 @@ val start_dependent_proof
   :  name:Names.Id.t
   -> udecl:UState.universe_decl
   -> poly:bool
+  -> info:Info.t
   -> Proofview.telescope
   -> Proof.t
 
@@ -247,33 +345,6 @@ val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
 
 type locality = Locality.locality = Discharge | Global of import_status
 
-(** Declaration hooks *)
-module Hook : sig
-  type t
-
-  (** Hooks allow users of the API to perform arbitrary actions at
-     proof/definition saving time. For example, to register a constant
-     as a Coercion, perform some cleanup, update the search database,
-     etc...  *)
-  module S : sig
-    type t =
-      { uctx : UState.t
-      (** [ustate]: universe constraints obtained when the term was closed *)
-      ; obls : (Id.t * Constr.t) list
-      (** [(n1,t1),...(nm,tm)]: association list between obligation
-          name and the corresponding defined term (might be a constant,
-          but also an arbitrary term in the Expand case of obligations) *)
-      ; scope : locality
-      (** [scope]: Locality of the original declaration *)
-      ; dref : GlobRef.t
-      (** [dref]: identifier of the original declaration *)
-      }
-  end
-
-  val make : (S.t -> unit) -> t
-  val call : ?hook:t -> S.t -> unit
-end
-
 (** XXX: This is an internal, low-level API and could become scheduled
     for removal from the public API, use higher-level declare APIs
     instead *)
@@ -317,21 +388,6 @@ val declare_assumption
   -> Entries.parameter_entry
   -> GlobRef.t
 
-module Recthm : sig
-  type t =
-    { name : Id.t
-    (** Name of theorem *)
-    ; typ : Constr.t
-    (** Type of theorem  *)
-    ; args : Name.t list
-    (** Names to pre-introduce  *)
-    ; impargs : Impargs.manual_implicits
-    (** Explicitily declared implicit arguments  *)
-    }
-end
-
-type lemma_possible_guards = int list list
-
 val declare_mutually_recursive
   : opaque:bool
   -> scope:locality
@@ -461,20 +517,6 @@ 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
@@ -495,59 +537,14 @@ val dependencies : Obligation.t array -> int -> Int.Set.t
 
 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
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index c0e30e926c..450699a1e8 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -13,38 +13,6 @@
 
 open Util
 
-(* Support for terminators and proofs with an associated constant
-   [that can be saved] *)
-
-type lemma_possible_guards = int list list
-
-module Proof_ending = Declare.Proof_ending
-module Info = Declare.Info
-
-(* Proofs with a save constant function *)
-type t =
-  { proof : Declare.Proof.t
-  ; info : Info.t
-  }
-
-let pf_map f pf = { pf with proof = f pf.proof }
-let pf_fold f pf = f pf.proof
-
-let set_endline_tactic t = pf_map (Declare.Proof.set_endline_tactic t)
-
-(* To be removed *)
-module Internal = struct
-
-  (** Gets the current terminator without checking that the proof has
-      been completed. Useful for the likes of [Admitted]. *)
-  let get_info ps = ps.info
-
-end
-
-let by tac pf =
-  let proof, res = Declare.by tac pf.proof in
-  { pf with proof }, res
-
 (************************************************************************)
 (* Creating a lemma-like constant                                       *)
 (************************************************************************)
@@ -52,19 +20,16 @@ let by tac pf =
 (* Starting a goal *)
 let start_lemma ~name ~poly
     ?(udecl=UState.default_univ_decl)
-    ?(info=Info.make ()) ?(impargs=[]) sigma c =
-  let proof = Declare.start_proof sigma ~name ~udecl ~poly c in
-  let info = Declare.Info.add_first_thm ~info ~name ~typ:c ~impargs in
-  { proof; info }
+    ?(info=Declare.Info.make ()) ?(impargs=[]) sigma c =
+  Declare.start_proof sigma ~name ~udecl ~poly ~impargs ~info c
 
 (* Note that proofs opened by start_dependent lemma cannot be closed
    by the regular terminators, thus we don't need to update the [thms]
    field. We will capture this invariant by typing in the future *)
 let start_dependent_lemma ~name ~poly
     ?(udecl=UState.default_univ_decl)
-    ?(info=Info.make ()) telescope =
-  let proof = Declare.start_dependent_proof ~name ~udecl ~poly telescope in
-  { proof; info }
+    ?(info=Declare.Info.make ()) telescope =
+  Declare.start_dependent_proof ~name ~udecl ~poly ~info telescope
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
@@ -102,15 +67,9 @@ 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.make ?hook ~scope ~kind ~compute_guard ~thms () in
+    let info = Declare.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
-
-let save_lemma_admitted ~lemma =
-  Declare.save_lemma_admitted ~proof:lemma.proof ~info:lemma.info
-
-let save_lemma_proved ~lemma ~opaque ~idopt =
-  Declare.save_lemma_proved ~proof:lemma.proof ~info:lemma.info ~opaque ~idopt
+    Declare.Proof.map ~f:(fun p ->
+        pi1 @@ Proof.run_tactic Global.(env ()) init_tac p) lemma
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 4787a940da..f882854862 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -12,45 +12,24 @@ open Names
 
 (** {4 Proofs attached to a constant} *)
 
-type t
-(** [Lemmas.t] represents a constant that is being proved, usually
-    interactively *)
-
-val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
-(** [set_endline_tactic tac lemma] set ending tactic for [lemma] *)
-
-val pf_map : (Declare.Proof.t -> Declare.Proof.t) -> t -> t
-(** [pf_map f l] map the underlying proof object *)
-
-val pf_fold : (Declare.Proof.t -> 'a) -> t -> 'a
-(** [pf_fold f l] fold over the underlying proof object *)
-
-val by : unit Proofview.tactic -> t -> t * bool
-(** [by tac l] apply a tactic to [l] *)
-
-module Proof_ending = Declare.Proof_ending
-module Info = Declare.Info
-
 (** Starts the proof of a constant *)
 val start_lemma
   :  name:Id.t
   -> poly:bool
   -> ?udecl:UState.universe_decl
-  -> ?info:Info.t
+  -> ?info:Declare.Info.t
   -> ?impargs:Impargs.manual_implicits
   -> Evd.evar_map
   -> EConstr.types
-  -> t
+  -> Declare.Proof.t
 
 val start_dependent_lemma
   :  name:Id.t
   -> poly:bool
   -> ?udecl:UState.universe_decl
-  -> ?info:Info.t
+  -> ?info:Declare.Info.t
   -> Proofview.telescope
-  -> t
-
-type lemma_possible_guards = int list list
+  -> Declare.Proof.t
 
 (** Pretty much internal, used by the Lemma / Fixpoint vernaculars *)
 val start_lemma_with_initialization
@@ -60,23 +39,7 @@ val start_lemma_with_initialization
   -> kind:Decls.logical_kind
   -> udecl:UState.universe_decl
   -> Evd.evar_map
-  -> (bool * lemma_possible_guards * Constr.t option list option) option
+  -> (bool * Declare.lemma_possible_guards * Constr.t option list option) option
   -> Declare.Recthm.t list
   -> int list option
-  -> t
-
-(** {4 Saving proofs} *)
-
-val save_lemma_admitted : lemma:t -> unit
-
-val save_lemma_proved
-  :  lemma:t
-  -> opaque:Declare.opacity_flag
-  -> idopt:Names.lident option
-  -> unit
-
-(** To be removed, don't use! *)
-module Internal : sig
-  val get_info : t -> Info.t
-  (** Only needed due to the Declare compatibility layer. *)
-end
+  -> Declare.Proof.t
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index a8eac8fd2d..05edb55760 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -142,13 +142,13 @@ let rec solve_obligation prg num tac =
   let auto n oblset tac = auto_solve_obligations n ~oblset tac in
   let proof_ending =
     Declare.Proof_ending.End_obligation
-      {Declare.Obls.name = prg.prg_name; num; auto}
+      {Declare.name = prg.prg_name; num; auto}
   in
-  let info = Lemmas.Info.make ~proof_ending ~scope ~kind () in
+  let info = Declare.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
-  let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in
+  let lemma = fst @@ Declare.by !default_tactic lemma in
+  let lemma = Option.cata (fun tac -> Declare.Proof.set_endline_tactic tac lemma) lemma tac in
   lemma
 
 and obligation (user_num, name, typ) tac =
@@ -243,7 +243,7 @@ and try_solve_obligations n tac =
   let _ = solve_obligations n tac in
   ()
 
-and auto_solve_obligations n ?oblset tac : progress =
+and auto_solve_obligations n ?oblset tac : Declare.progress =
   Flags.if_verbose Feedback.msg_info
     (str "Solving obligations automatically...");
   let prg = get_unique_prog n in
@@ -320,13 +320,13 @@ let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl)
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose (msg_generating_obl name) obls;
     let cst = Declare.Obls.declare_definition prg in
-    Defined cst)
+    Declare.Defined cst)
   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 ->
+    | Declare.Remain rem ->
       Flags.if_verbose (show_obligations ~msg:false) (Some name);
       res
     | _ -> res
@@ -354,7 +354,7 @@ let add_mutual_definitions l ~uctx ?(udecl = UState.default_univ_decl)
         else
           let res = auto_solve_obligations (Some x) tactic in
           match res with
-          | Defined _ ->
+          | Declare.Defined _ ->
             (* If one definition is turned into a constant,
                the whole block is defined. *)
             (pm, true)
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index c21951373b..f0a8e9bea1 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
-  -> Declare.Obls.progress
+  -> Declare.progress
 
 (* XXX: unify with MutualEntry *)
 
@@ -109,15 +109,15 @@ val add_mutual_definitions :
 val obligation :
      int * Names.Id.t option * Constrexpr.constr_expr option
   -> Genarg.glob_generic_argument option
-  -> Lemmas.t
+  -> Declare.Proof.t
 
 (** Implementation of the [Next Obligation] command *)
 val next_obligation :
-  Names.Id.t option -> Genarg.glob_generic_argument option -> Lemmas.t
+  Names.Id.t option -> Genarg.glob_generic_argument option -> Declare.Proof.t
 
 (** Implementation of the [Solve Obligation] command *)
 val solve_obligations :
-  Names.Id.t option -> unit Proofview.tactic option -> Declare.Obls.progress
+  Names.Id.t option -> unit Proofview.tactic option -> Declare.progress
 
 val solve_all_obligations : unit Proofview.tactic option -> unit
 
diff --git a/vernac/proof_global.ml b/vernac/proof_global.ml
index 0c5bc39020..2c66b3e26c 100644
--- a/vernac/proof_global.ml
+++ b/vernac/proof_global.ml
@@ -2,9 +2,9 @@
 
 type t = Declare.Proof.t
 [@@ocaml.deprecated "Use [Declare.Proof.t]"]
-let map_proof = Declare.Proof.map_proof
+let map_proof = Declare.Proof.map
 [@@ocaml.deprecated "Use [Declare.Proof.map_proof]"]
-let get_proof = Declare.Proof.get_proof
+let get_proof = Declare.Proof.get
 [@@ocaml.deprecated "Use [Declare.Proof.get_proof]"]
 
 type opacity_flag = Declare.opacity_flag =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9a1d935928..a3dd1856aa 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -94,7 +94,7 @@ let show_proof ~pstate =
   (* spiwack: this would probably be cooler with a bit of polishing. *)
   try
     let pstate = Option.get pstate in
-    let p = Declare.Proof.get_proof pstate in
+    let p = Declare.Proof.get pstate in
     let sigma, _ = Declare.get_current_context pstate in
     let pprf = Proof.partial_proof p in
     (* In the absence of an environment explicitly attached to the
@@ -595,15 +595,15 @@ let vernac_start_proof ~atts kind l =
 
 let vernac_end_proof ~lemma = let open Vernacexpr in function
   | Admitted ->
-    Lemmas.save_lemma_admitted ~lemma
+    Declare.save_lemma_admitted ~proof:lemma
   | Proved (opaque,idopt) ->
-    Lemmas.save_lemma_proved ~lemma ~opaque ~idopt
+    Declare.save_lemma_proved ~proof:lemma ~opaque ~idopt
 
 let vernac_exact_proof ~lemma c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the beginning of a proof. *)
-  let lemma, status = Lemmas.by (Tactics.exact_proof c) lemma in
-  let () = Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Opaque ~idopt:None in
+  let lemma, status = Declare.by (Tactics.exact_proof c) lemma in
+  let () = Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Opaque ~idopt:None in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
@@ -1187,7 +1187,7 @@ let focus_command_cond = Proof.no_cond command_focus
      all tactics fail if there are no further goals to prove. *)
 
 let vernac_solve_existential ~pstate n com =
-  Declare.Proof.map_proof (fun p ->
+  Declare.Proof.map ~f:(fun p ->
       let intern env sigma = Constrintern.intern_constr env sigma com in
       Proof.V82.instantiate_evar (Global.env ()) n intern p) pstate
 
@@ -1200,7 +1200,7 @@ let vernac_set_end_tac ~pstate tac =
 let vernac_set_used_variables ~pstate e : Declare.Proof.t =
   let env = Global.env () in
   let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
-  let tys = List.map snd (initial_goals (Declare.Proof.get_proof pstate)) in
+  let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in
   let tys = List.map EConstr.Unsafe.to_constr tys in
   let l = Proof_using.process_expr env e tys in
   let vars = Environ.named_context env in
@@ -1668,7 +1668,7 @@ let vernac_global_check c =
 
 
 let get_nth_goal ~pstate n =
-  let pf = Declare.Proof.get_proof pstate in
+  let pf = Declare.Proof.get pstate in
   let Proof.{goals;sigma} = Proof.data pf in
   let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in
   gl
@@ -1747,7 +1747,7 @@ let vernac_print ~pstate ~atts =
   | PrintHintGoal ->
      begin match pstate with
      | Some pstate ->
-       let pf = Declare.Proof.get_proof pstate in
+       let pf = Declare.Proof.get pstate in
        Hints.pr_applicable_hint pf
      | None ->
        str "No proof in progress"
@@ -1833,7 +1833,7 @@ let vernac_register qid r =
 (* Proof management *)
 
 let vernac_focus ~pstate gln =
-  Declare.Proof.map_proof (fun p ->
+  Declare.Proof.map ~f:(fun p ->
     match gln with
       | None -> Proof.focus focus_command_cond () 1 p
       | Some 0 ->
@@ -1844,13 +1844,13 @@ let vernac_focus ~pstate gln =
 
   (* Unfocuses one step in the focus stack. *)
 let vernac_unfocus ~pstate =
-  Declare.Proof.map_proof
-    (fun p -> Proof.unfocus command_focus p ())
+  Declare.Proof.map
+    ~f:(fun p -> Proof.unfocus command_focus p ())
     pstate
 
 (* Checks that a proof is fully unfocused. Raises an error if not. *)
 let vernac_unfocused ~pstate =
-  let p = Declare.Proof.get_proof pstate in
+  let p = Declare.Proof.get pstate in
   if Proof.unfocused p then
     str"The proof is indeed fully unfocused."
   else
@@ -1863,7 +1863,7 @@ let subproof_kind = Proof.new_focus_kind ()
 let subproof_cond = Proof.done_cond subproof_kind
 
 let vernac_subproof gln ~pstate =
-  Declare.Proof.map_proof (fun p ->
+  Declare.Proof.map ~f:(fun p ->
     match gln with
     | None -> Proof.focus subproof_cond () 1 p
     | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
@@ -1873,12 +1873,12 @@ let vernac_subproof gln ~pstate =
     pstate
 
 let vernac_end_subproof ~pstate =
-  Declare.Proof.map_proof (fun p ->
+  Declare.Proof.map ~f:(fun p ->
       Proof.unfocus subproof_kind p ())
     pstate
 
 let vernac_bullet (bullet : Proof_bullet.t) ~pstate =
-  Declare.Proof.map_proof (fun p ->
+  Declare.Proof.map ~f:(fun p ->
     Proof_bullet.put p bullet) pstate
 
 (* Stack is needed due to show proof names, should deprecate / remove
@@ -1895,7 +1895,7 @@ let vernac_show ~pstate =
     end
   (* Show functions that require a proof state *)
   | Some pstate ->
-    let proof = Declare.Proof.get_proof pstate in
+    let proof = Declare.Proof.get pstate in
     begin function
     | ShowGoal goalref ->
       begin match goalref with
@@ -1907,14 +1907,14 @@ let vernac_show ~pstate =
     | ShowUniverses -> show_universes ~proof
     (* Deprecate *)
     | ShowProofNames ->
-      Id.print (Declare.Proof.get_proof_name pstate)
+      Id.print (Declare.Proof.get_name pstate)
     | ShowIntros all -> show_intro ~proof all
     | ShowProof -> show_proof ~pstate:(Some pstate)
     | ShowMatch id -> show_match id
     end
 
 let vernac_check_guard ~pstate =
-  let pts = Declare.Proof.get_proof pstate in
+  let pts = Declare.Proof.get pstate in
   let pfterm = List.hd (Proof.partial_proof pts) in
   let message =
     try
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index d772f274a2..f8a80e8feb 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -55,8 +55,8 @@ and proof_block_name = string (** open type of delimiters *)
 type typed_vernac =
   | VtDefault of (unit -> unit)
   | VtNoProof of (unit -> unit)
-  | VtCloseProof of (lemma:Lemmas.t -> unit)
-  | VtOpenProof of (unit -> Lemmas.t)
+  | VtCloseProof of (lemma:Declare.Proof.t -> unit)
+  | VtOpenProof of (unit -> Declare.Proof.t)
   | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t)
   | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
   | VtReadProof of (pstate:Declare.Proof.t -> unit)
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 58c267080a..103e24233b 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -73,8 +73,8 @@ and proof_block_name = string (** open type of delimiters *)
 type typed_vernac =
   | VtDefault of (unit -> unit)
   | VtNoProof of (unit -> unit)
-  | VtCloseProof of (lemma:Lemmas.t -> unit)
-  | VtOpenProof of (unit -> Lemmas.t)
+  | VtCloseProof of (lemma:Declare.Proof.t -> unit)
+  | VtOpenProof of (unit -> Declare.Proof.t)
   | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t)
   | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
   | VtReadProof of (pstate:Declare.Proof.t -> unit)
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 7ab21141df..09cb9e4c8c 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -39,14 +39,14 @@ let interp_typed_vernac c ~stack =
   | VtOpenProof f ->
     Some (Vernacstate.LemmaStack.push stack (f ()))
   | VtModifyProof f ->
-    Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack
+    Option.map (Vernacstate.LemmaStack.map_top ~f:(fun pstate -> f ~pstate)) stack
   | VtReadProofOpt f ->
-    let pstate = Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:(fun x -> x)) stack in
+    let pstate = Option.map (Vernacstate.LemmaStack.with_top ~f:(fun x -> x)) stack in
     f ~pstate;
     stack
   | VtReadProof f ->
     vernac_require_open_lemma ~stack
-      (Vernacstate.LemmaStack.with_top_pstate ~f:(fun pstate -> f ~pstate));
+      (Vernacstate.LemmaStack.with_top ~f:(fun pstate -> f ~pstate));
     stack
 
 (* Default proof mode, to be set at the beginning of proofs for
@@ -202,7 +202,7 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) =
        let before_univs = Global.universes () in
        let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in
        if before_univs == Global.universes () then pstack
-       else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Declare.Proof.update_global_env) pstack)
+       else Option.map (Vernacstate.LemmaStack.map_top ~f:Declare.Proof.update_global_env) pstack)
     ~st
 
 (* XXX: This won't properly set the proof mode, as of today, it is
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index e3e708e87d..675dfd11f3 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -15,7 +15,7 @@ val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control ->
    proof and won't be forced *)
 val interp_qed_delayed_proof
   :  proof:Declare.proof_object
-  -> info:Lemmas.Info.t
+  -> info:Declare.Info.t
   -> st:Vernacstate.t
   -> control:Vernacexpr.control_flag list
   -> Vernacexpr.proof_end CAst.t
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 0fca1e9078..5968e6a982 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -26,18 +26,16 @@ end
 
 module LemmaStack = struct
 
-  type t = Lemmas.t * Lemmas.t list
+  type t = Declare.Proof.t * Declare.Proof.t list
 
   let map f (pf, pfl) = (f pf, List.map f pfl)
-
-  let map_top_pstate ~f (pf, pfl) = (Lemmas.pf_map f pf, pfl)
+  let map_top ~f (pf, pfl) = (f pf, pfl)
 
   let pop (ps, p) = match p with
     | [] -> ps, None
     | pp :: p -> ps, Some (pp, p)
 
   let with_top (p, _) ~f = f p
-  let with_top_pstate (p, _) ~f = Lemmas.pf_fold f p
 
   let push ontop a =
     match ontop with
@@ -45,12 +43,12 @@ module LemmaStack = struct
     | Some (l,ls) -> a, (l :: ls)
 
   let get_all_proof_names (pf : t) =
-    let prj x = Lemmas.pf_fold Declare.Proof.get_proof x in
+    let prj x = Declare.Proof.get x in
     let (pn, pns) = map Proof.(function pf -> (data (prj pf)).name) pf in
     pn :: pns
 
   let copy_info src tgt =
-    Lemmas.pf_map (fun _ -> Lemmas.pf_fold (fun x -> x) tgt) src
+    Declare.Proof.map ~f:(fun _ -> Declare.Proof.fold ~f:(fun x -> x) tgt) src
 
   let copy_info ~src ~tgt =
     let (ps, psl), (ts,tsl) = src, tgt in
@@ -111,7 +109,7 @@ module Declare = struct
   let set x = s_lemmas := x
 
   let get_pstate () =
-    Option.map (LemmaStack.with_top ~f:(Lemmas.pf_fold (fun x -> x))) !s_lemmas
+    Option.map (LemmaStack.with_top ~f:(fun x -> x)) !s_lemmas
 
   let freeze ~marshallable:_ = get ()
   let unfreeze x = s_lemmas := Some x
@@ -125,15 +123,8 @@ module Declare = struct
       | _ -> None
     end
 
-  open Lemmas
-  open Declare
-
   let cc f = match !s_lemmas with
     | None -> raise NoCurrentProof
-    | Some x -> LemmaStack.with_top_pstate ~f x
-
-  let cc_lemma f = match !s_lemmas with
-    | None -> raise NoCurrentProof
     | Some x -> LemmaStack.with_top ~f x
 
   let cc_stack f = match !s_lemmas with
@@ -142,41 +133,41 @@ module Declare = struct
 
   let dd f = match !s_lemmas with
     | None -> raise NoCurrentProof
-    | Some x -> s_lemmas := Some (LemmaStack.map_top_pstate ~f x)
+    | Some x -> s_lemmas := Some (LemmaStack.map_top ~f x)
 
   let there_are_pending_proofs () = !s_lemmas <> None
-  let get_open_goals () = cc Proof.get_open_goals
+  let get_open_goals () = cc Declare.Proof.get_open_goals
 
-  let give_me_the_proof_opt () = Option.map (LemmaStack.with_top_pstate ~f:Proof.get_proof) !s_lemmas
-  let give_me_the_proof () = cc Proof.get_proof
-  let get_current_proof_name () = cc Proof.get_proof_name
+  let give_me_the_proof_opt () = Option.map (LemmaStack.with_top ~f:Declare.Proof.get) !s_lemmas
+  let give_me_the_proof () = cc Declare.Proof.get
+  let get_current_proof_name () = cc Declare.Proof.get_name
 
-  let map_proof f = dd (Proof.map_proof f)
+  let map_proof f = dd (Declare.Proof.map ~f)
   let with_current_proof f =
     match !s_lemmas with
     | None -> raise NoCurrentProof
     | Some stack ->
-      let pf, res = LemmaStack.with_top_pstate stack ~f:(Proof.map_fold_proof_endline f) in
-      let stack = LemmaStack.map_top_pstate stack ~f:(fun _ -> pf) in
+      let pf, res = LemmaStack.with_top stack ~f:(Declare.Proof.map_fold_endline ~f) in
+      let stack = LemmaStack.map_top stack ~f:(fun _ -> pf) in
       s_lemmas := Some stack;
       res
 
-  type closed_proof = Declare.proof_object * Lemmas.Info.t
+  type closed_proof = Declare.proof_object * Declare.Info.t
 
 
-  let return_proof () = cc return_proof
-  let return_partial_proof () = cc return_partial_proof
+  let return_proof () = cc Declare.return_proof
+  let return_partial_proof () = cc Declare.return_partial_proof
 
   let close_future_proof ~feedback_id pf =
-    cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~feedback_id st pf) pt,
-                        Lemmas.Internal.get_info pt)
+    cc (fun pt -> Declare.close_future_proof ~feedback_id pt pf,
+                  Declare.Proof.get_info pt)
 
   let close_proof ~opaque ~keep_body_ucst_separate =
-    cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate)) pt,
-                        Lemmas.Internal.get_info pt)
+    cc (fun pt -> Declare.close_proof ~opaque ~keep_body_ucst_separate pt,
+                  Declare.Proof.get_info pt)
 
   let discard_all () = s_lemmas := None
-  let update_global_env () = dd (Proof.update_global_env)
+  let update_global_env () = dd (Declare.Proof.update_global_env)
 
   let get_current_context () = cc Declare.get_current_context
 
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index fb6d8b6db6..07c27dd849 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -22,11 +22,11 @@ module LemmaStack : sig
 
   type t
 
-  val pop : t -> Lemmas.t * t option
-  val push : t option -> Lemmas.t -> t
+  val pop : t -> Declare.Proof.t * t option
+  val push : t option -> Declare.Proof.t -> t
 
-  val map_top_pstate : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t
-  val with_top_pstate : t -> f:(Declare.Proof.t -> 'a ) -> 'a
+  val map_top : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t
+  val with_top : t -> f:(Declare.Proof.t -> 'a ) -> 'a
 
 end
 
@@ -68,7 +68,7 @@ module Declare : sig
   val return_proof : unit -> Declare.closed_proof_output
   val return_partial_proof : unit -> Declare.closed_proof_output
 
-  type closed_proof = Declare.proof_object * Lemmas.Info.t
+  type closed_proof = Declare.proof_object * Declare.Info.t
 
   val close_future_proof :
     feedback_id:Stateid.t ->