[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.

35 files changed, 367 insertions, 448 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 8c2090f3be..dee407bbe4 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -287,7 +287,7 @@ VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
 | ![ proof_query ] [ "ExploreProof" ] ->
   { fun ~pstate ->
     let sigma, env = Declare.get_current_context pstate in
-    let pprf = Proof.partial_proof (Declare.Proof.get_proof pstate) in
+    let pprf = Proof.partial_proof (Declare.Proof.get pstate) in
     Feedback.msg_notice
       (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
   }
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index e5665c59b8..633d5dfe3b 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -15,7 +15,7 @@ open Context.Named.Declaration
     (which can contain references to [f]) in the context extended by
     [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
     and [lemma] as the proof. *)
-let start_deriving f suchthat name : Lemmas.t =
+let start_deriving f suchthat name : Declare.Proof.t =
 
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -40,8 +40,7 @@ let start_deriving f suchthat name : Lemmas.t =
                 TNil sigma))))))
   in
 
-  let info = Lemmas.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
+  let info = Declare.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
-  end) lemma
+  Declare.Proof.map lemma ~f:(fun p ->
+      Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index ef94c7e78f..06e7dacd36 100644
--- a/plugins/derive/derive.mli
+++ b/plugins/derive/derive.mli
@@ -16,4 +16,4 @@ val start_deriving
   :  Names.Id.t
   -> Constrexpr.constr_expr
   -> Names.Id.t
-  -> Lemmas.t
+  -> Declare.Proof.t
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index a0627dbe63..39c6c4ea54 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -729,13 +729,13 @@ let extract_and_compile l =
 (* Show the extraction of the current ongoing proof *)
 let show_extraction ~pstate =
   init ~inner:true false false;
-  let prf = Declare.Proof.get_proof pstate in
+  let prf = Declare.Proof.get pstate in
   let sigma, env = Declare.get_current_context pstate in
   let trms = Proof.partial_proof prf in
   let extr_term t =
     let ast, ty = extract_constr env sigma t in
     let mp = Lib.current_mp () in
-    let l = Label.of_id (Declare.Proof.get_proof_name pstate) in
+    let l = Label.of_id (Declare.Proof.get_name pstate) in
     let fake_ref = GlobRef.ConstRef (Constant.make2 mp l) in
     let decl = Dterm (fake_ref, ast, ty) in
     print_one_decl [] mp decl
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index b864b18887..652f942cb9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -856,9 +856,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let lemma =
     Lemmas.start_lemma ~name:(mk_equation_id f_id) ~poly:false evd lemma_type
   in
-  let lemma, _ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in
+  let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in
   let () =
-    Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None
+    Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent
+      ~idopt:None
   in
   evd
 
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 608155eb71..2336689a66 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1520,10 +1520,10 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let typ, _ = lemmas_types_infos.(i) in
           let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false !evd typ in
           let lemma =
-            fst @@ Lemmas.by (Proofview.V82.tactic (proving_tac i)) lemma
+            fst @@ Declare.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
           let () =
-            Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent
+            Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent
               ~idopt:None
           in
           let finfo =
@@ -1586,7 +1586,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           in
           let lemma =
             fst
-              (Lemmas.by
+              (Declare.by
                  (Proofview.V82.tactic
                     (observe_tac
                        ("prove completeness (" ^ Id.to_string f_id ^ ")")
@@ -1594,7 +1594,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
                  lemma)
           in
           let () =
-            Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent
+            Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent
               ~idopt:None
           in
           let finfo =
@@ -1769,7 +1769,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt
     using_lemmas args ret_type body
 
 let do_generate_principle_aux pconstants on_error register_built
-    interactive_proof fixpoint_exprl : Lemmas.t option =
+    interactive_proof fixpoint_exprl : Declare.Proof.t option =
   List.iter
     (fun {Vernacexpr.notations} ->
       if not (List.is_empty notations) then
@@ -2155,7 +2155,7 @@ let make_graph (f_ref : GlobRef.t) =
 
 (* *************** statically typed entrypoints ************************* *)
 
-let do_generate_principle_interactive fixl : Lemmas.t =
+let do_generate_principle_interactive fixl : Declare.Proof.t =
   match do_generate_principle_aux [] warning_error true true fixl with
   | Some lemma -> lemma
   | None ->
diff --git a/plugins/funind/gen_principle.mli b/plugins/funind/gen_principle.mli
index 3c04d6cb7d..28751c4501 100644
--- a/plugins/funind/gen_principle.mli
+++ b/plugins/funind/gen_principle.mli
@@ -12,7 +12,7 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 
 val do_generate_principle_interactive :
-  Vernacexpr.fixpoint_expr list -> Lemmas.t
+  Vernacexpr.fixpoint_expr list -> Declare.Proof.t
 
 val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit
 val make_graph : Names.GlobRef.t -> unit
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9b2d9c4815..f92d4c6a72 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -58,7 +58,7 @@ let declare_fun name kind ?univs value =
     (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce))
 
 let defined lemma =
-  Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None
+  Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent ~idopt:None
 
 let def_of_const t =
   match Constr.kind t with
@@ -1343,7 +1343,7 @@ let whole_start concl_tac nb_args is_mes func input_type relation rec_arg_num :
     g
 
 let get_current_subgoals_types pstate =
-  let p = Declare.Proof.get_proof pstate in
+  let p = Declare.Proof.get pstate in
   let Proof.{goals = sgs; sigma; _} = Proof.data p in
   (sigma, List.map (Goal.V82.abstract_type sigma) sgs)
 
@@ -1405,7 +1405,7 @@ let clear_goals sigma =
   List.map clear_goal
 
 let build_new_goal_type lemma =
-  let sigma, sub_gls_types = Lemmas.pf_fold get_current_subgoals_types lemma in
+  let sigma, sub_gls_types = get_current_subgoals_types lemma in
   (* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
   let sub_gls_types = clear_goals sigma sub_gls_types in
   (* Pp.msgnl (str "sub_gls_types2 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
@@ -1423,7 +1423,7 @@ let is_opaque_constant c =
 let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
     (gls_type, decompose_and_tac, nb_goal) =
   (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
-  let current_proof_name = Lemmas.pf_fold Declare.Proof.get_proof_name lemma in
+  let current_proof_name = Declare.Proof.get_name lemma in
   let name =
     match goal_name with
     | Some s -> s
@@ -1488,18 +1488,18 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
                      [Hints.Hint_db.empty TransparentState.empty false] ]))
     in
     let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
-    Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None
+    Declare.save_lemma_proved ~proof:lemma ~opaque:opacity ~idopt:None
   in
-  let info = Lemmas.Info.make ~hook:(Declare.Hook.make hook) () in
+  let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in
   let lemma =
     Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type
   in
   let lemma =
     if Indfun_common.is_strict_tcc () then
-      fst @@ Lemmas.by (Proofview.V82.tactic tclIDTAC) lemma
+      fst @@ Declare.by (Proofview.V82.tactic tclIDTAC) lemma
     else
       fst
-      @@ Lemmas.by
+      @@ Declare.by
            (Proofview.V82.tactic (fun g ->
                 tclTHEN decompose_and_tac
                   (tclORELSE
@@ -1521,27 +1521,26 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
                   g))
            lemma
   in
-  if Lemmas.(pf_fold Declare.Proof.get_open_goals) lemma = 0 then (
-    defined lemma; None )
+  if Declare.Proof.get_open_goals lemma = 0 then (defined lemma; None)
   else Some lemma
 
 let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
     fonctional_ref input_type relation rec_arg_num thm_name using_lemmas nb_args
     ctx hook =
   let start_proof env ctx tac_start tac_end =
-    let info = Lemmas.Info.make ~hook () in
+    let info = Declare.Info.make ~hook () in
     let lemma =
       Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) ~info ctx
         (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
     in
     let lemma =
       fst
-      @@ Lemmas.by
+      @@ Declare.by
            (New.observe_tac (fun _ _ -> str "starting_tac") tac_start)
            lemma
     in
     fst
-    @@ Lemmas.by
+    @@ Declare.by
          (Proofview.V82.tactic
             (observe_tac
                (fun _ _ -> str "whole_start")
@@ -1608,7 +1607,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   in
   let lemma =
     fst
-    @@ Lemmas.by
+    @@ Declare.by
          (Proofview.V82.tactic
             (start_equation f_ref terminate_ref (fun x ->
                  prove_eq
@@ -1642,7 +1641,8 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   in
   let _ =
     Flags.silently
-      (fun () -> Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None)
+      (fun () ->
+        Declare.save_lemma_proved ~proof:lemma ~opaque:opacity ~idopt:None)
       ()
   in
   ()
@@ -1651,7 +1651,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
 
 let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
     type_of_f r rec_arg_num eq generate_induction_principle using_lemmas :
-    Lemmas.t option =
+    Declare.Proof.t option =
   let open Term in
   let open Constr in
   let open CVars in
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 4e5146e37c..2612f2b63e 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -25,4 +25,4 @@ val recursive_definition :
       -> EConstr.constr
       -> unit)
   -> Constrexpr.constr_expr list
-  -> Lemmas.t option
+  -> Declare.Proof.t option
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index ffb597d4cb..40c64a1c26 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -918,7 +918,7 @@ END
 VERNAC COMMAND EXTEND GrabEvars STATE proof
 | [ "Grab" "Existential" "Variables" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
+  -> { fun ~pstate -> Declare.Proof.map ~f:(fun p -> Proof.V82.grab_evars p) pstate }
 END
 
 (* Shelves all the goals under focus. *)
@@ -950,7 +950,7 @@ END
 VERNAC COMMAND EXTEND Unshelve STATE proof
 | [ "Unshelve" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Declare.Proof.map_proof (fun p  -> Proof.unshelve p) pstate  }
+  -> { fun ~pstate -> Declare.Proof.map ~f:(fun p  -> Proof.unshelve p) pstate  }
 END
 
 (* Gives up on the goals under focus: the goals are considered solved,
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 996f6b3eb3..114acaa412 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -363,7 +363,7 @@ let print_info_trace =
 
 let vernac_solve ~pstate n info tcom b =
   let open Goal_select in
-  let pstate, status = Declare.Proof.map_fold_proof_endline (fun etac p ->
+  let pstate, status = Declare.Proof.map_fold_endline ~f:(fun etac p ->
       let with_end_tac = if b then Some etac else None in
       let global = match n with SelectAll | SelectList _ -> true | _ -> false in
       let info = Option.append info (print_info_trace ()) in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 4bc8d61258..e784d6e682 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1978,7 +1978,7 @@ let add_morphism_as_parameter atts m n : unit =
        (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global cst);
   declare_projection n instance_id cst
 
-let add_morphism_interactive atts m n : Lemmas.t =
+let add_morphism_interactive atts m n : Declare.Proof.t =
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
   let env = Global.env () in
@@ -1996,11 +1996,11 @@ let add_morphism_interactive atts m n : Lemmas.t =
     | _ -> assert false
   in
   let hook = Declare.Hook.make hook in
-  let info = Lemmas.Info.make ~hook ~kind () in
+  let info = Declare.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->
        let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info evd morph in
-       fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
+       fst (Declare.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
   init_setoid ();
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 1161c84e6a..60a66dd861 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -101,7 +101,7 @@ val add_setoid
   -> Id.t
   -> unit
 
-val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Lemmas.t
+val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Declare.Proof.t
 val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit
 
 val add_morphism
@@ -110,7 +110,7 @@ val add_morphism
   -> constr_expr
   -> constr_expr
   -> Id.t
-  -> Lemmas.t
+  -> Declare.Proof.t
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
 
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 2ff76e69f8..3d892fa5ca 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -49,8 +49,8 @@ let is_focused_goal_simple ~doc id =
   match state_of_id ~doc id with
   | `Expired | `Error _ | `Valid None -> `Not
   | `Valid (Some { Vernacstate.lemmas }) ->
-    Option.cata (Vernacstate.LemmaStack.with_top_pstate ~f:(fun proof ->
-        let proof = Declare.Proof.get_proof proof in
+    Option.cata (Vernacstate.LemmaStack.with_top ~f:(fun proof ->
+        let proof = Declare.Proof.get proof in
         let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in
         let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
         if List.for_all (fun x -> simple_goal sigma x rest) focused
diff --git a/stm/stm.ml b/stm/stm.ml
index 943c83ecd3..7aaa359149 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1157,7 +1157,8 @@ end = struct (* {{{ *)
 
   let get_proof ~doc id =
     match state_of_id ~doc id with
-    | `Valid (Some vstate) -> Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:Declare.Proof.get_proof) vstate.Vernacstate.lemmas
+    | `Valid (Some vstate) ->
+      Option.map (Vernacstate.LemmaStack.with_top ~f:Declare.Proof.get) vstate.Vernacstate.lemmas
     | _ -> None
 
   let undo_vernac_classifier v ~doc =
@@ -1526,7 +1527,7 @@ end = struct (* {{{ *)
           try
             let _pstate =
               stm_qed_delay_proof ~st ~id:stop
-                ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None)) in
+                ~proof:pobject ~info:(Declare.Info.make ()) ~loc ~control:[] (Proved (opaque,None)) in
             ()
           with exn ->
             (* If [stm_qed_delay_proof] fails above we need to use the
@@ -1672,7 +1673,7 @@ end = struct (* {{{ *)
       let proof, _info =
         PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in
 
-      let info = Lemmas.Info.make () in
+      let info = Declare.Info.make () in
 
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 987cd8c1b8..0a6e976db8 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -808,7 +808,7 @@ let perform_eval ~pstate e =
       Goal_select.SelectAll, Proof.start ~name ~poly sigma []
     | Some pstate ->
       Goal_select.get_default_goal_selector (),
-      Declare.Proof.get_proof pstate
+      Declare.Proof.get pstate
   in
   let v = match selector with
   | Goal_select.SelectNth i -> Proofview.tclFOCUS i i v
@@ -912,15 +912,15 @@ let print_ltac qid =
 (** Calling tactics *)
 
 let solve ~pstate default tac =
-  let pstate, status = Declare.Proof.map_fold_proof_endline begin fun etac p ->
+  let pstate, status = Declare.Proof.map_fold_endline pstate ~f:(fun etac p ->
     let with_end_tac = if default then Some etac else None in
     let g = Goal_select.get_default_goal_selector () in
     let (p, status) = Proof.solve g None tac ?with_end_tac p in
     (* in case a strict subtree was completed,
        go back to the top of the prooftree *)
     let p = Proof.maximal_unfocus Vernacentries.command_focus p in
-    p, status
-  end pstate in
+    p, status)
+  in
   if not status then Feedback.feedback Feedback.AddedAxiom;
   pstate
 
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 ->