Merge PR #12372: [declare] Refactor constant information into a record.

Reviewed-by: SkySkimmer

57 files changed, 1952 insertions, 2211 deletions

diff --git a/dev/base_include b/dev/base_include
index efbd156758..67ea3a1fa1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -111,10 +111,8 @@ open Search
 open Evar_refiner
 open Goal
 open Logic
-open Pfedit
 open Proof
 open Proof_using
-open Proof_global
 open Redexpr
 open Refiner
 open Tacmach
diff --git a/dev/ci/user-overlays/12372-ejgallego-proof+info.sh b/dev/ci/user-overlays/12372-ejgallego-proof+info.sh
new file mode 100644
index 0000000000..b9fdc338b5
--- /dev/null
+++ b/dev/ci/user-overlays/12372-ejgallego-proof+info.sh
@@ -0,0 +1,24 @@
+if [ "$CI_PULL_REQUEST" = "12372" ] || [ "$CI_BRANCH" = "proof+info" ]; then
+
+    rewriter_CI_REF=proof+info
+    rewriter_CI_GITURL=https://github.com/ejgallego/rewriter
+
+    paramcoq_CI_REF=proof+info
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+    mtac2_CI_REF=proof+info
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+    equations_CI_REF=proof+info
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    elpi_CI_REF=proof+info
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    aac_tactics_CI_REF=proof+info
+    aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics
+
+    metacoq_CI_REF=proof+info
+    metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
+
+fi
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 8c2090f3be..d24d968c01 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -286,8 +286,8 @@ END
 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 sigma, env = Declare.Proof.get_current_context 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/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index e9e866c5fb..4d0105ea9d 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,6 +1,7 @@
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
-  let scope = Declare.Global Declare.ImportDefaultBehavior in
+  let scope = Locality.Global Locality.ImportDefaultBehavior in
   let kind = Decls.(IsDefinition Definition) in
-  Declare.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl
-    ~opaque:false ~poly ~types:None ~body sigma
+  let cinfo = Declare.CInfo.make ~name ~typ:None () in
+  let info = Declare.Info.make ~scope ~kind  ~udecl ~poly () in
+  Declare.declare_definition ~info ~cinfo ~opaque:false ~body sigma
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index bd99cbed1b..2adc35ae3e 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -343,7 +343,7 @@ let search flags =
   let pstate = Vernacstate.Declare.get_pstate () in
   let sigma, env = match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
-  | Some p -> Declare.get_goal_context p 1 in
+  | Some p -> Declare.Proof.get_goal_context p 1 in
   List.map export_coq_object (Search.interface_search env sigma (
     List.map (fun (c, b) -> (import_search_constraint c, b)) flags)
   )
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index e5665c59b8..027064b75f 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 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
+  let info = Declare.Info.make ~poly ~kind () in
+  let lemma = Declare.Proof.start_derive ~name ~f ~info goals in
+  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..af43c0517e 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 sigma, env = Declare.get_current_context pstate in
+  let prf = Declare.Proof.get pstate in
+  let sigma, env = Declare.Proof.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..2151ad7873 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -853,12 +853,16 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
 
   (*i The next call to mk_equation_id is valid since we are
      constructing the lemma Ensures by: obvious i*)
-  let lemma =
-    Lemmas.start_lemma ~name:(mk_equation_id f_id) ~poly:false evd lemma_type
+  let info = Declare.Info.make () in
+  let cinfo =
+    Declare.CInfo.make ~name:(mk_equation_id f_id) ~typ:lemma_type ()
+  in
+  let lemma = Declare.Proof.start ~cinfo ~info evd in
+  let lemma, _ =
+    Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
   in
-  let lemma, _ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in
-  let () =
-    Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None
+  let (_ : _ list) =
+    Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
   in
   evd
 
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 608155eb71..167cf37026 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -319,7 +319,7 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts
     let entry = Declare.definition_entry ~univs ?types body in
     let (_ : Names.GlobRef.t) =
       Declare.declare_entry ~name:new_princ_name ~hook
-        ~scope:(Declare.Global Declare.ImportDefaultBehavior)
+        ~scope:(Locality.Global Locality.ImportDefaultBehavior)
         ~kind:Decls.(IsProof Theorem)
         ~impargs:[] ~uctx entry
     in
@@ -400,7 +400,7 @@ let register_struct is_rec fixpoint_exprl =
           Pp.(str "Body of Function must be given")
     in
     ComDefinition.do_definition ~name:fname.CAst.v ~poly:false
-      ~scope:(Declare.Global Declare.ImportDefaultBehavior)
+      ~scope:(Locality.Global Locality.ImportDefaultBehavior)
       ~kind:Decls.Definition univs binders None body (Some rtype);
     let evd, rev_pconstants =
       List.fold_left
@@ -419,7 +419,7 @@ let register_struct is_rec fixpoint_exprl =
     (None, evd, List.rev rev_pconstants)
   | _ ->
     ComFixpoint.do_fixpoint
-      ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false
+      ~scope:(Locality.Global Locality.ImportDefaultBehavior) ~poly:false
       fixpoint_exprl;
     let evd, rev_pconstants =
       List.fold_left
@@ -1370,12 +1370,12 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list =
       | None -> raise Not_found
       | Some finfos -> finfos
     in
-    let open Declare in
     match finfos.equation_lemma with
-    | None -> Transparent (* non recursive definition *)
+    | None -> Vernacexpr.Transparent (* non recursive definition *)
     | Some equation ->
-      if Declareops.is_opaque (Global.lookup_constant equation) then Opaque
-      else Transparent
+      if Declareops.is_opaque (Global.lookup_constant equation) then
+        Vernacexpr.Opaque
+      else Vernacexpr.Transparent
   in
   let body, typ, univs, _hook, sigma0 =
     try
@@ -1518,12 +1518,14 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
             i*)
           let lem_id = mk_correct_id f_id in
           let typ, _ = lemmas_types_infos.(i) in
-          let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false !evd typ in
+          let info = Declare.Info.make () in
+          let cinfo = Declare.CInfo.make ~name:lem_id ~typ () in
+          let lemma = Declare.Proof.start ~cinfo ~info !evd in
           let lemma =
-            fst @@ Lemmas.by (Proofview.V82.tactic (proving_tac i)) lemma
+            fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
-          let () =
-            Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent
+          let (_ : GlobRef.t list) =
+            Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
               ~idopt:None
           in
           let finfo =
@@ -1580,21 +1582,22 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
               Ensures by: obvious
             i*)
           let lem_id = mk_complete_id f_id in
-          let lemma =
-            Lemmas.start_lemma ~name:lem_id ~poly:false sigma
-              (fst lemmas_types_infos.(i))
+          let info = Declare.Info.make () in
+          let cinfo =
+            Declare.CInfo.make ~name:lem_id ~typ:(fst lemmas_types_infos.(i)) ()
           in
+          let lemma = Declare.Proof.start ~cinfo sigma ~info in
           let lemma =
             fst
-              (Lemmas.by
+              (Declare.Proof.by
                  (Proofview.V82.tactic
                     (observe_tac
                        ("prove completeness (" ^ Id.to_string f_id ^ ")")
                        (proving_tac i)))
                  lemma)
           in
-          let () =
-            Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent
+          let (_ : _ list) =
+            Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
               ~idopt:None
           in
           let finfo =
@@ -1769,7 +1772,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 +2158,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 ->
@@ -2199,7 +2202,7 @@ let build_scheme fas =
   List.iter2
     (fun (princ_id, _, _) (body, types, univs, opaque) ->
       let (_ : Constant.t) =
-        let opaque = if opaque = Declare.Opaque then true else false in
+        let opaque = if opaque = Vernacexpr.Opaque then true else false in
         let def_entry = Declare.definition_entry ~univs ~opaque ?types body in
         Declare.declare_constant ~name:princ_id
           ~kind:Decls.(IsProof Theorem)
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..884792cc15 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -58,7 +58,10 @@ 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
+  let (_ : _ list) =
+    Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
+  in
+  ()
 
 let def_of_const t =
   match Constr.kind t with
@@ -1343,7 +1346,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 +1408,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); *)
@@ -1414,16 +1417,17 @@ let build_new_goal_type lemma =
 
 let is_opaque_constant c =
   let cb = Global.lookup_constant c in
+  let open Vernacexpr in
   match cb.Declarations.const_body with
-  | Declarations.OpaqueDef _ -> Declare.Opaque
-  | Declarations.Undef _ -> Declare.Opaque
-  | Declarations.Def _ -> Declare.Transparent
-  | Declarations.Primitive _ -> Declare.Opaque
+  | Declarations.OpaqueDef _ -> Opaque
+  | Declarations.Undef _ -> Opaque
+  | Declarations.Def _ -> Transparent
+  | Declarations.Primitive _ -> Opaque
 
 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 +1492,20 @@ 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
-  in
-  let info = Lemmas.Info.make ~hook:(Declare.Hook.make hook) () in
-  let lemma =
-    Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type
+    let (_ : _ list) =
+      Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
+    in
+    ()
   in
+  let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in
+  let cinfo = Declare.CInfo.make ~name:na ~typ:gls_type () in
+  let lemma = Declare.Proof.start ~cinfo ~info sigma in
   let lemma =
     if Indfun_common.is_strict_tcc () then
-      fst @@ Lemmas.by (Proofview.V82.tactic tclIDTAC) lemma
+      fst @@ Declare.Proof.by (Proofview.V82.tactic tclIDTAC) lemma
     else
       fst
-      @@ Lemmas.by
+      @@ Declare.Proof.by
            (Proofview.V82.tactic (fun g ->
                 tclTHEN decompose_and_tac
                   (tclORELSE
@@ -1521,27 +1527,28 @@ 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 lemma =
-      Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) ~info ctx
-        (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
+    let cinfo =
+      Declare.CInfo.make ~name:thm_name
+        ~typ:(EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
+        ()
     in
+    let info = Declare.Info.make ~hook () in
+    let lemma = Declare.Proof.start ~cinfo ~info ctx in
     let lemma =
       fst
-      @@ Lemmas.by
+      @@ Declare.Proof.by
            (New.observe_tac (fun _ _ -> str "starting_tac") tac_start)
            lemma
     in
     fst
-    @@ Lemmas.by
+    @@ Declare.Proof.by
          (Proofview.V82.tactic
             (observe_tac
                (fun _ _ -> str "whole_start")
@@ -1602,13 +1609,16 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   let evd = Evd.from_ctx uctx in
   let f_constr = constr_of_monomorphic_global f_ref in
   let equation_lemma_type = subst1 f_constr equation_lemma_type in
-  let lemma =
-    Lemmas.start_lemma ~name:eq_name ~poly:false evd
-      (EConstr.of_constr equation_lemma_type)
+  let info = Declare.Info.make () in
+  let cinfo =
+    Declare.CInfo.make ~name:eq_name
+      ~typ:(EConstr.of_constr equation_lemma_type)
+      ()
   in
+  let lemma = Declare.Proof.start ~cinfo evd ~info in
   let lemma =
     fst
-    @@ Lemmas.by
+    @@ Declare.Proof.by
          (Proofview.V82.tactic
             (start_equation f_ref terminate_ref (fun x ->
                  prove_eq
@@ -1642,7 +1652,7 @@ 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.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None)
       ()
   in
   ()
@@ -1651,7 +1661,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/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 498b33d1a8..81ee6ed5bb 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -28,7 +28,7 @@ let () =
   let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
     snd (get_default_tactic ())
   end in
-  Obligations.default_tactic := tac
+  Declare.Obls.default_tactic := tac
 
 let with_tac f tac =
   let env = Genintern.empty_glob_sign (Global.env ()) in
@@ -78,10 +78,10 @@ GRAMMAR EXTEND Gram
 
 {
 
-open Obligations
+open Declare.Obls
 
-let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
-let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
+let obligation obl tac = with_tac (fun t -> obligation obl t) tac
+let next_obligation obl tac = with_tac (fun t -> next_obligation obl t) tac
 
 let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 4bc8d61258..f16d0717df 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1900,10 +1900,12 @@ let declare_projection name instance_id r =
     in it_mkProd_or_LetIn ccl ctx
   in
   let types = Some (it_mkProd_or_LetIn typ ctx) in
-  let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in
+  let kind, opaque, scope = Decls.(IsDefinition Definition), false, Locality.Global Locality.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
+  let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
+  let info = Declare.Info.make ~scope ~kind ~udecl ~poly () in
   let _r : GlobRef.t =
-    Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
+    Declare.declare_definition ~cinfo ~info ~opaque ~body sigma
   in ()
 
 let build_morphism_signature env sigma m =
@@ -1967,7 +1969,7 @@ let add_morphism_as_parameter atts m n : unit =
   let env = Global.env () in
   let evd = Evd.from_env env in
   let poly = atts.polymorphic in
-  let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in
+  let kind, opaque, scope = Decls.(IsAssumption Logical), false, Locality.Global Locality.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
   let evd, types = build_morphism_signature env evd m in
   let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in
@@ -1978,7 +1980,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 +1998,12 @@ 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
   Flags.silently
     (fun () ->
-       let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info evd morph in
-       fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
+       let cinfo = Declare.CInfo.make ~name:instance_id ~typ:morph () in
+       let info = Declare.Info.make ~poly ~hook ~kind () in
+       let lemma = Declare.Proof.start ~cinfo ~info evd in
+       fst (Declare.Proof.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/proofs/proof.ml b/proofs/proof.ml
index 175c487958..a183fa7797 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -120,7 +120,7 @@ type t =
   ; name : Names.Id.t
   (** the name of the theorem whose proof is being constructed *)
   ; poly : bool
-  (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *)
+  (** polymorphism *)
   }
 
 (*** General proof functions ***)
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..652d064b83 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -147,7 +147,7 @@ let update_global_env () =
     PG_compat.update_global_env ()
 
 module Vcs_ = Vcs.Make(Stateid.Self)
-type future_proof = Declare.closed_proof_output Future.computation
+type future_proof = Declare.Proof.closed_proof_output Future.computation
 
 type depth = int
 type branch_type =
@@ -1047,9 +1047,9 @@ end = struct (* {{{ *)
 end (* }}} *)
 
 (* Wrapper for the proof-closing special path for Qed *)
-let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc ~control pending : Vernacstate.t =
+let stm_qed_delay_proof ?route ~proof ~pinfo ~id ~st ~loc ~control pending : Vernacstate.t =
   set_id_for_feedback ?route dummy_doc id;
-  Vernacinterp.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending)
+  Vernacinterp.interp_qed_delayed_proof ~proof ~pinfo ~st ~control (CAst.make ?loc pending)
 
 (* Wrapper for Vernacentries.interp to set the feedback id *)
 (* It is currently called 19 times, this number should be certainly
@@ -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 =
@@ -1351,7 +1352,7 @@ module rec ProofTask : sig
     t_stop     : Stateid.t;
     t_drop     : bool;
     t_states   : competence;
-    t_assign   : Declare.closed_proof_output Future.assignment -> unit;
+    t_assign   : Declare.Proof.closed_proof_output Future.assignment -> unit;
     t_loc      : Loc.t option;
     t_uuid     : Future.UUID.t;
     t_name     : string }
@@ -1374,7 +1375,7 @@ module rec ProofTask : sig
     ?loc:Loc.t ->
     drop_pt:bool ->
     Stateid.t * Stateid.t -> Stateid.t ->
-      Declare.closed_proof_output Future.computation
+      Declare.Proof.closed_proof_output Future.computation
 
   (* If set, only tasks overlapping with this list are processed *)
   val set_perspective : Stateid.t list -> unit
@@ -1390,7 +1391,7 @@ end = struct (* {{{ *)
     t_stop     : Stateid.t;
     t_drop     : bool;
     t_states   : competence;
-    t_assign   : Declare.closed_proof_output Future.assignment -> unit;
+    t_assign   : Declare.Proof.closed_proof_output Future.assignment -> unit;
     t_loc      : Loc.t option;
     t_uuid     : Future.UUID.t;
     t_name     : string }
@@ -1412,7 +1413,7 @@ end = struct (* {{{ *)
     e_safe_states : Stateid.t list }
 
   type response =
-    | RespBuiltProof of Declare.closed_proof_output * float
+    | RespBuiltProof of Declare.Proof.closed_proof_output * float
     | RespError of error
     | RespStates of (Stateid.t * State.partial_state) list
 
@@ -1522,11 +1523,12 @@ end = struct (* {{{ *)
             PG_compat.close_future_proof ~feedback_id:stop (Future.from_val proof) in
 
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
-          let opaque = Declare.Opaque in
+          let opaque = Opaque in
           try
             let _pstate =
+              let pinfo = Declare.Proof.Proof_info.default () in
               stm_qed_delay_proof ~st ~id:stop
-                ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None)) in
+                ~proof:pobject ~pinfo ~loc ~control:[] (Proved (opaque,None)) in
             ()
           with exn ->
             (* If [stm_qed_delay_proof] fails above we need to use the
@@ -1666,13 +1668,13 @@ end = struct (* {{{ *)
         let _proof = PG_compat.return_partial_proof () in
         `OK_ADMITTED
       else begin
-      let opaque = Declare.Opaque in
+      let opaque = Opaque in
 
       (* The original terminator, a hook, has not been saved in the .vio*)
       let proof, _info =
         PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in
 
-      let info = Lemmas.Info.make () in
+      let pinfo = Declare.Proof.Proof_info.default () 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 *)
@@ -1685,9 +1687,9 @@ end = struct (* {{{ *)
        *)
       (* STATE We use the state resulting from reaching start. *)
       let st = Vernacstate.freeze_interp_state ~marshallable:false in
-      ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None)));
+      ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~pinfo ~loc ~control:[] (Proved (opaque,None)));
       (* Is this name the same than the one in scope? *)
-      let name = Declare.get_po_name proof in
+      let name = Declare.Proof.get_po_name proof in
       `OK name
       end
     with e ->
@@ -2161,7 +2163,7 @@ let collect_proof keep cur hd brkind id =
    | id :: _ -> Names.Id.to_string id in
  let loc = (snd cur).expr.CAst.loc in
  let is_defined_expr = function
-   | VernacEndProof (Proved (Declare.Transparent,_)) -> true
+   | VernacEndProof (Proved (Transparent,_)) -> true
    | _ -> false in
  let is_defined = function
    | _, { expr = e } -> is_defined_expr e.CAst.v.expr
@@ -2496,13 +2498,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                       | VtKeepDefined ->
                         CErrors.anomaly (Pp.str "Cannot delegate transparent proofs, this is a bug in the STM.")
                     in
-                    let proof, info =
+                    let proof, pinfo =
                       PG_compat.close_future_proof ~feedback_id:id fp in
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
                     let st = Vernacstate.freeze_interp_state ~marshallable:false in
                     let control, pe = extract_pe x in
-                    ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe);
+                    ignore(stm_qed_delay_proof ~id ~st ~proof ~pinfo ~loc ~control pe);
                     feedback ~id:id Incomplete
                 | { VCS.kind = `Master }, _ -> assert false
                 end;
@@ -2526,7 +2528,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                   | VtKeep VtKeepAxiom ->
                       qed.fproof <- Some (None, ref false); None
                   | VtKeep opaque ->
-                    let opaque = let open Declare in  match opaque with
+                    let opaque = match opaque with
                       | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent
                       | VtKeepAxiom -> assert false
                     in
@@ -2541,9 +2543,9 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                 let st = Vernacstate.freeze_interp_state ~marshallable:false in
                 let _st = match proof with
                   | None ->  stm_vernac_interp id st x
-                  | Some (proof, info) ->
+                  | Some (proof, pinfo) ->
                     let control, pe = extract_pe x in
-                    stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe
+                    stm_qed_delay_proof ~id ~st ~proof ~pinfo ~loc ~control pe
                 in
                 let wall_clock3 = Unix.gettimeofday () in
                 Aux_file.record_in_aux_at ?loc:x.expr.CAst.loc "proof_check_time"
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index cf127648b4..a957f7354f 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -37,7 +37,7 @@ let string_of_vernac_classification = function
   | VtMeta -> "Meta "
   | VtProofMode _ -> "Proof Mode"
 
-let vtkeep_of_opaque = let open Declare in function
+let vtkeep_of_opaque = function
   | Opaque -> VtKeepOpaque
   | Transparent -> VtKeepDefined
 
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..ba08aa2b94 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -311,12 +311,13 @@ let instance_hook info global ?hook cst =
   declare_instance env sigma (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype =
+let declare_instance_constant iinfo global impargs ?hook name udecl poly sigma term termtype =
   let kind = Decls.(IsDefinition Instance) in
-  let scope = Declare.Global Declare.ImportDefaultBehavior in
-  let kn = Declare.declare_definition ~name ~kind ~scope ~impargs
-      ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in
-  instance_hook info global ?hook kn
+  let scope = Locality.Global Locality.ImportDefaultBehavior in
+  let cinfo = Declare.CInfo.make ~name ~impargs ~typ:(Some termtype) () in
+  let info = Declare.Info.make ~kind ~scope ~poly ~udecl () in
+  let kn = Declare.declare_definition ~cinfo ~info ~opaque:false ~body:term sigma in
+  instance_hook iinfo global ?hook kn
 
 let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name =
   let subst = List.fold_left2
@@ -344,9 +345,12 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term
   let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in
   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 scope, kind = Locality.Global Locality.ImportDefaultBehavior,
+                    Decls.IsDefinition Decls.Instance in
+  let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+  let info = Declare.Info.make  ~udecl ~scope ~poly ~kind ~hook () in
   let _ : Declare.Obls.progress =
-    Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls
+    Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls
   in ()
 
 let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype =
@@ -358,11 +362,12 @@ 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 ~udecl ~poly () 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
-  let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info ~impargs sigma termtype in
+  let cinfo = Declare.CInfo.make ~name:id ~impargs ~typ:termtype () in
+  let lemma = Declare.Proof.start ~cinfo ~info sigma in
   (* spiwack: I don't know what to do with the status here. *)
   let lemma =
     match term with
@@ -374,15 +379,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.Proof.by init_refine lemma in
       lemma
     | None ->
-      let lemma, _ = Lemmas.by (Tactics.auto_intros_tac ids) lemma in
+      let lemma, _ = Declare.Proof.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.Proof.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/comAssumption.ml b/vernac/comAssumption.ml
index 44c30598aa..d8475126ca 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -61,8 +61,8 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name
   let sigma = Evd.from_env env in
   let () = if do_instance then Classes.declare_instance env sigma None false gr in
   let local = match local with
-    | Declare.ImportNeedQualified -> true
-    | Declare.ImportDefaultBehavior -> false
+    | Locality.ImportNeedQualified -> true
+    | Locality.ImportDefaultBehavior -> false
   in
   let () = if is_coe then ComCoercion.try_add_new_coercion gr ~local ~poly in
   let inst = instance_of_univ_entry univs in
@@ -86,11 +86,11 @@ let context_set_of_entry = function
   | Monomorphic_entry uctx -> uctx
 
 let declare_assumptions ~poly ~scope ~kind univs nl l =
-  let () = let open Declare in match scope with
-    | Discharge ->
+  let () = match scope with
+    | Locality.Discharge ->
       (* declare universes separately for variables *)
       DeclareUctx.declare_universe_context ~poly (context_set_of_entry (fst univs))
-    | Global _ -> ()
+    | Locality.Global _ -> ()
   in
   let _, _ = List.fold_left (fun (subst,univs) ((is_coe,idl),typ,imps) ->
       (* NB: here univs are ignored when scope=Discharge *)
@@ -98,10 +98,10 @@ let declare_assumptions ~poly ~scope ~kind univs nl l =
       let univs,subst' =
         List.fold_left_map (fun univs id ->
             let refu = match scope with
-              | Declare.Discharge ->
+              | Locality.Discharge ->
                 declare_variable is_coe ~kind typ imps Glob_term.Explicit id;
                 GlobRef.VarRef id.CAst.v, Univ.Instance.empty
-              | Declare.Global local ->
+              | Locality.Global local ->
                 declare_axiom is_coe ~local ~poly ~kind typ univs imps nl id
             in
             next_univs univs, (id.CAst.v, Constr.mkRef refu))
@@ -128,9 +128,8 @@ let process_assumptions_udecls ~scope l =
       udecl, id
     | (_, ([], _))::_ | [] -> assert false
   in
-  let open Declare in
   let () = match scope, udecl with
-    | Discharge, Some _ ->
+    | Locality.Discharge, Some _ ->
       let loc = first_id.CAst.loc in
       let msg = Pp.str "Section variables cannot be polymorphic." in
       user_err ?loc  msg
@@ -174,7 +173,7 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l =
       uvars, (coe,t,imps))
       Univ.LSet.empty l
   in
-  (* XXX: Using `DeclareDef.prepare_parameter` here directly is not
+  (* XXX: Using `Declare.prepare_parameter` here directly is not
      possible as we indeed declare several parameters; however,
      restrict_universe_context should be called in a centralized place
      IMO, thus I think we should adapt `prepare_parameter` to handle
@@ -202,11 +201,11 @@ let context_insection sigma ~poly ctx =
           else Monomorphic_entry Univ.ContextSet.empty
         in
         let entry = Declare.definition_entry ~univs ~types:t b in
-        (* XXX Fixme: Use DeclareDef.prepare_definition *)
+        (* XXX Fixme: Use Declare.prepare_definition *)
         let uctx = Evd.evar_universe_context sigma in
         let kind = Decls.(IsDefinition Definition) in
         let _ : GlobRef.t =
-          Declare.declare_entry ~name ~scope:Declare.Discharge
+          Declare.declare_entry ~name ~scope:Locality.Discharge
             ~kind ~impargs:[] ~uctx entry
         in
         ()
@@ -237,8 +236,8 @@ let context_nosection sigma ~poly ctx =
         let entry = Declare.definition_entry ~univs ~types:t b in
         Declare.DefinitionEntry entry
     in
-    let local = if Lib.is_modtype () then Declare.ImportDefaultBehavior
-      else Declare.ImportNeedQualified
+    let local = if Lib.is_modtype () then Locality.ImportDefaultBehavior
+      else Locality.ImportNeedQualified
     in
     let cst = Declare.declare_constant ~name ~kind ~local decl in
     let () = Declare.assumption_message name in
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 989015a9f3..3d425ad768 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -17,7 +17,7 @@ open Constrexpr
 val do_assumptions
   :  program_mode:bool
   -> poly:bool
-  -> scope:Declare.locality
+  -> scope:Locality.locality
   -> kind:Decls.assumption_object_kind
   -> Declaremods.inline
   -> (ident_decl list * constr_expr) with_coercion list
@@ -35,7 +35,7 @@ val declare_variable
 val declare_axiom
   : coercion_flag
   -> poly:bool
-  -> local:Declare.import_status
+  -> local:Locality.import_status
   -> kind:Decls.assumption_object_kind
   -> Constr.types
   -> Entries.universes_entry * UnivNames.universe_binders
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index 3cc5dd65af..15d8ebc4b5 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -354,7 +354,7 @@ let try_add_new_coercion_with_source ref ~local ~poly ~source =
   try_add_new_coercion_core ref ~local poly (Some source) None false
 
 let add_coercion_hook poly { Declare.Hook.S.scope; dref; _ } =
-  let open Declare in
+  let open Locality in
   let local = match scope with
   | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
@@ -367,7 +367,7 @@ let add_coercion_hook poly { Declare.Hook.S.scope; dref; _ } =
 let add_coercion_hook ~poly = Declare.Hook.make (add_coercion_hook poly)
 
 let add_subclass_hook ~poly { Declare.Hook.S.scope; dref; _ } =
-  let open Declare in
+  let open Locality in
   let stre = match scope with
   | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index d56917271c..f9b2d8b1d1 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -116,9 +116,10 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
   let kind = Decls.IsDefinition kind in
+  let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
+  let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly () in
   let _ : Names.GlobRef.t =
-    Declare.declare_definition ~name ~scope ~kind ?hook ~impargs
-      ~opaque:false ~poly evd ~udecl ~types ~body
+    Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd
   in ()
 
 let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
@@ -126,8 +127,9 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c
   let (body, types), evd, udecl, impargs =
     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 term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
   let _ : Declare.Obls.progress =
-    Obligations.add_definition
-      ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls
+    let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+    let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in
+    Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls
   in ()
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 2e8fe16252..e3417d0062 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -17,7 +17,7 @@ open Constrexpr
 val do_definition
   :  ?hook:Declare.Hook.t
   -> name:Id.t
-  -> scope:Declare.locality
+  -> scope:Locality.locality
   -> poly:bool
   -> kind:Decls.definition_object_kind
   -> universe_decl_expr option
@@ -30,9 +30,9 @@ val do_definition
 val do_definition_program
   :  ?hook:Declare.Hook.t
   -> name:Id.t
-  -> scope:Declare.locality
+  -> scope:Locality.locality
   -> poly:bool
-  -> kind:Decls.definition_object_kind
+  -> kind:Decls.logical_kind
   -> universe_decl_expr option
   -> local_binder_expr list
   -> red_expr option
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 0b75e7f410..0f34adf1c7 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -257,11 +257,9 @@ let build_recthms ~indexes fixnames fixtypes fiximps =
   in
   let thms =
     List.map3 (fun name typ (ctx,impargs,_) ->
-        { Declare.Recthm.name
-        ; typ
-        ; args = List.map Context.Rel.Declaration.get_name ctx
-        ; impargs})
-      fixnames fixtypes fiximps
+        let args = List.map Context.Rel.Declaration.get_name ctx in
+        Declare.CInfo.make ~name ~typ ~args ~impargs ()
+      ) fixnames fixtypes fiximps
   in
   fix_kind, cofix, thms
 
@@ -270,9 +268,10 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   let indexes = Option.default [] indexes in
   let init_terms = Some fixdefs in
   let evd = Evd.from_ctx ctx in
+  let info = Declare.Info.make ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl () in
   let lemma =
-    Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl
-      evd (Some(cofix,indexes,init_terms)) thms None in
+    Declare.Proof.start_mutual_with_initialization ~info
+      evd ~mutual_info:(cofix,indexes,init_terms) ~cinfo:thms None in
   (* Declare notations *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   lemma
@@ -283,10 +282,11 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let fixdefs = List.map Option.get fixdefs in
   let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
   let fix_kind = Decls.IsDefinition fix_kind in
+  let info = Declare.Info.make ~scope ~kind:fix_kind ~poly ~udecl () in
+  let cinfo = fixitems in
   let _ : GlobRef.t list =
-    Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx
-      ~possible_indexes:indexes ~udecl ~ntns ~rec_declaration
-      fixitems
+    Declare.declare_mutually_recursive ~cinfo ~info ~opaque:false ~uctx
+      ~possible_indexes:indexes ~ntns ~rec_declaration
   in
   ()
 
@@ -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..aa5446205c 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -16,16 +16,16 @@ 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:Locality.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t
 
 val do_fixpoint :
-  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit
+  scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit
 
 val do_cofixpoint_interactive :
-  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t
+  scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t
 
 val do_cofixpoint :
-  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit
+  scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit
 
 (************************************************************************)
 (** Internal API  *)
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index ec37ec7fa8..b05bf9a675 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -56,7 +56,7 @@ let project_hint ~poly pri l2r r =
     Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c))
   in
   let c =
-    Declare.declare_constant ~local:Declare.ImportDefaultBehavior ~name
+    Declare.declare_constant ~local:Locality.ImportDefaultBehavior ~name
       ~kind:Decls.(IsDefinition Definition)
       cb
   in
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index e490b33dde..673124296d 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -657,5 +657,3 @@ let make_cases ind =
        let consref = GlobRef.ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
        (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
     mip.mind_nf_lc []
-
-let declare_mutual_inductive_with_eliminations = DeclareInd.declare_mutual_inductive_with_eliminations
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 984581152a..9c876787a3 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -41,14 +41,6 @@ val do_mutual_inductive
 
 val make_cases : Names.inductive -> string list list
 
-val declare_mutual_inductive_with_eliminations
-  : ?primitive_expected:bool
-  -> Entries.mutual_inductive_entry
-  -> UnivNames.universe_binders
-  -> DeclareInd.one_inductive_impls list
-  -> Names.MutInd.t
-  [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"]
-
 val interp_mutual_inductive_constr
   : sigma:Evd.evar_map
   -> template:bool option
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 4aa46e0a86..37615fa09c 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -260,8 +260,11 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
     RetrieveObl.retrieve_obligations env recname sigma 0 def typ
   in
   let uctx = Evd.evar_universe_context sigma in
-  ignore(Obligations.add_definition ~name:recname ~term:evars_def ~udecl
-           ~poly evars_typ ~uctx evars ~hook)
+  let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in
+  let info = Declare.Info.make ~udecl ~poly ~hook () in
+  let _ : Declare.Obls.progress =
+    Declare.Obls.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in
+  ()
 
 let out_def = function
   | Some def -> def
@@ -290,7 +293,8 @@ let do_program_recursive ~scope ~poly fixkind fixl =
     let evars, _, def, typ =
       RetrieveObl.retrieve_obligations env name evm
         (List.length rec_sign) def typ in
-    ({ Declare.Recthm.name; typ; impargs; args = [] }, def, evars)
+    let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+    (cinfo, def, evars)
   in
   let (fixnames,fixrs,fixdefs,fixtypes) = fix in
   let fiximps = List.map pi2 info in
@@ -314,11 +318,12 @@ let do_program_recursive ~scope ~poly fixkind fixl =
   end in
   let uctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
-  | Declare.Obls.IsFixpoint _ -> Decls.Fixpoint
-  | Declare.Obls.IsCoFixpoint -> Decls.CoFixpoint
+  | Declare.Obls.IsFixpoint _ -> Decls.(IsDefinition Fixpoint)
+  | Declare.Obls.IsCoFixpoint -> Decls.(IsDefinition CoFixpoint)
   in
   let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
-  Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind
+  let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in
+  Declare.Obls.add_mutual_definitions defs ~info ~uctx ~ntns fixkind
 
 let do_fixpoint ~scope ~poly l =
   let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index 8b1fa6c202..e39f62c348 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -14,8 +14,8 @@ open Vernacexpr
 
 val do_fixpoint :
   (* When [false], assume guarded. *)
-  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit
+  scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit
 
 val do_cofixpoint :
   (* When [false], assume guarded. *)
-  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit
+  scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 59922c662a..6326a22e83 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -16,111 +16,76 @@ open Names
 open Safe_typing
 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 =
-  { endline_tactic : Genarg.glob_generic_argument option
-  ; section_vars : Id.Set.t option
-  ; proof : Proof.t
-  ; udecl: UState.universe_decl
-  (** Initial universe declarations *)
-  ; initial_euctx : UState.t
-  (** The initial universe context (for the statement) *)
-  }
+  type t = (S.t -> unit) CEphemeron.key
 
-(*** Proof Global manipulation ***)
+  let make hook = CEphemeron.create hook
 
-let get_proof ps = ps.proof
-let get_proof_name ps = (Proof.data ps.proof).Proof.name
+  let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook
 
-let get_initial_euctx ps = ps.initial_euctx
+end
 
-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
+module CInfo = struct
 
-let map_fold_proof_endline f ps =
-  let et =
-    match ps.endline_tactic with
-    | None -> Proofview.tclUNIT ()
-    | Some tac ->
-      let open Geninterp in
-      let {Proof.poly} = Proof.data ps.proof in
-      let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in
-      let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
-      let tac = Geninterp.interp tag ist tac in
-      Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
-  in
-  let (newpr,ret) = f et ps.proof in
-  let ps = { ps with proof = newpr } in
-  ps, ret
+  type 'constr t =
+    { name : Id.t
+    (** Name of theorem *)
+    ; typ : 'constr
+    (** Type of theorem  *)
+    ; args : Name.t list
+    (** Names to pre-introduce  *)
+    ; impargs : Impargs.manual_implicits
+    (** Explicitily declared implicit arguments  *)
+    }
 
-let compact_the_proof pf = map_proof Proof.compact pf
 
-(* Sets the tactic to be used when a tactic line is closed with [...] *)
-let set_endline_tactic tac ps =
-  { ps with endline_tactic = Some tac }
+  let make ~name ~typ ?(args=[]) ?(impargs=[]) () =
+    { name; typ; args; impargs }
 
-(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
-   name [name] with goals [goals] (a list of pairs of environment and
-   conclusion). The proof is started in the evar map [sigma] (which
-   can typically contain universe constraints), and with universe
-   bindings [udecl]. *)
-let start_proof ~name ~udecl ~poly sigma goals =
-  let proof = Proof.start ~name ~poly sigma goals in
-  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
-  { proof
-  ; endline_tactic = None
-  ; section_vars = None
-  ; udecl
-  ; initial_euctx
-  }
+  let to_constr sigma thm = { thm with typ = EConstr.to_constr sigma thm.typ }
 
-let start_dependent_proof ~name ~udecl ~poly goals =
-  let proof = Proof.dependent_start ~name ~poly goals in
-  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
-  { proof
-  ; endline_tactic = None
-  ; section_vars = None
-  ; udecl
-  ; initial_euctx
-  }
+  let get_typ { typ; _ } = typ
+  let get_name { name; _ } = name
 
-let get_used_variables pf = pf.section_vars
-let get_universe_decl pf = pf.udecl
+end
 
-let set_used_variables ps l =
-  let open Context.Named.Declaration in
-  let env = Global.env () in
-  let ids = List.fold_right Id.Set.add l Id.Set.empty in
-  let ctx = Environ.keep_hyps env ids in
-  let ctx_set =
-    List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
-  let vars_of = Environ.global_vars_set in
-  let aux env entry (ctx, all_safe as orig) =
-    match entry with
-    | LocalAssum ({Context.binder_name=x},_) ->
-       if Id.Set.mem x all_safe then orig
-       else (ctx, all_safe)
-    | LocalDef ({Context.binder_name=x},bo, ty) as decl ->
-       if Id.Set.mem x all_safe then orig else
-       let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
-       if Id.Set.subset vars all_safe
-       then (decl :: ctx, Id.Set.add x all_safe)
-       else (ctx, all_safe) in
-  let ctx, _ =
-    Environ.fold_named_context aux env ~init:(ctx,ctx_set) in
-  if not (Option.is_empty ps.section_vars) then
-    CErrors.user_err Pp.(str "Used section variables can be declared only once");
-  ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) }
+(** Information for a declaration, interactive or not, includes
+   parameters shared by mutual constants *)
+module Info = struct
 
-let get_open_goals ps =
-  let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
-  List.length goals +
-  List.fold_left (+) 0
-    (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
-  List.length shelf
+  type t =
+    { poly : bool
+    ; inline : bool
+    ; kind : Decls.logical_kind
+    ; udecl : UState.universe_decl
+    ; scope : Locality.locality
+    ; hook : Hook.t option
+    }
+
+  (** Note that [opaque] doesn't appear here as it is not known at the
+     start of the proof in the interactive case. *)
+  let make ?(poly=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition))
+      ?(udecl=UState.default_univ_decl) ?(scope=Locality.Global Locality.ImportDefaultBehavior)
+      ?hook () =
+    { poly; inline; kind; udecl; scope; hook }
 
-type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeedQualified
+end
 
 (** Declaration of constants and parameters *)
 
@@ -153,117 +118,6 @@ let definition_entry_core ?(opaque=false) ?(inline=false) ?feedback_id ?section_
 let definition_entry =
   definition_entry_core ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None
 
-type proof_object =
-  { name : Names.Id.t
-  (* [name] only used in the STM *)
-  ; entries : Evd.side_effects proof_entry list
-  ; uctx: UState.t
-  }
-
-let get_po_name { name } = name
-
-let private_poly_univs =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Private";"Polymorphic";"Universes"]
-    ~value:true
-
-(* XXX: This is still separate from close_proof below due to drop_pt in the STM *)
-(* XXX: Unsafe_typ:true is needed by vio files, see bf0499bc507d5a39c3d5e3bf1f69191339270729 *)
-let prepare_proof ~unsafe_typ { proof } =
-  let Proof.{name=pid;entry;poly} = Proof.data proof in
-  let initial_goals = Proofview.initial_goals entry in
-  let evd = Proof.return ~pid proof in
-  let eff = Evd.eval_side_effects evd in
-  let evd = Evd.minimize_universes evd in
-  let to_constr_body c =
-    match EConstr.to_constr_opt evd c with
-    | Some p ->
-      Vars.universes_of_constr p, p
-    | None ->
-      CErrors.user_err Pp.(str "Some unresolved existential variables remain")
-  in
-  let to_constr_typ t =
-    if unsafe_typ
-    then
-      let t = EConstr.Unsafe.to_constr t in
-      Vars.universes_of_constr t, t
-    else to_constr_body t
-  in
-  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
-     side-effects... This may explain why one need to uniquize side-effects
-     thereafter... *)
-  (* EJGA: actually side-effects de-duplication and this codepath is
-     unrelated. Duplicated side-effects arise from incorrect scheme
-     generation code, the main bulk of it was mostly fixed by #9836
-     but duplication can still happen because of rewriting schemes I
-     think; however the code below is mostly untested, the only
-     code-paths that generate several proof entries are derive and
-     equations and so far there is no code in the CI that will
-     actually call those and do a side-effect, TTBOMK *)
-  (* EJGA: likely the right solution is to attach side effects to the first constant only? *)
-  let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in
-  proofs, Evd.evar_universe_context evd
-
-let make_univs_deferred ~poly ~initial_euctx ~uctx ~udecl
-    (used_univs_typ, typ) (used_univs_body, body) =
-  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-  let utyp = UState.univ_entry ~poly initial_euctx in
-  let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
-  (* For vi2vo compilation proofs are computed now but we need to
-     complement the univ constraints of the typ with the ones of
-     the body.  So we keep the two sets distinct. *)
-  let uctx_body = UState.restrict uctx used_univs in
-  let ubody = UState.check_mono_univ_decl uctx_body udecl in
-  utyp, ubody
-
-let make_univs_private_poly ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body) =
-  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-  let universes = UState.restrict uctx used_univs in
-  let typus = UState.restrict universes used_univs_typ in
-  let utyp = UState.check_univ_decl ~poly typus udecl in
-  let ubody = Univ.ContextSet.diff
-      (UState.context_set universes)
-      (UState.context_set typus)
-  in
-  utyp, ubody
-
-let make_univs ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body) =
-  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-  (* Since the proof is computed now, we can simply have 1 set of
-     constraints in which we merge the ones for the body and the ones
-     for the typ. We recheck the declaration after restricting with
-     the actually used universes.
-     TODO: check if restrict is really necessary now. *)
-  let ctx = UState.restrict uctx used_univs in
-  let utyp = UState.check_univ_decl ~poly ctx udecl in
-  utyp, Univ.ContextSet.empty
-
-let close_proof ~opaque ~keep_body_ucst_separate ps =
-
-  let { section_vars; proof; udecl; initial_euctx } = ps in
-  let { Proof.name; poly } = Proof.data proof in
-  let unsafe_typ = keep_body_ucst_separate && not poly in
-  let elist, uctx = prepare_proof ~unsafe_typ ps in
-  let opaque = match opaque with Opaque -> true | Transparent -> false in
-
-  let make_entry ((((_ub, body) as b), eff), ((_ut, typ) as t)) =
-    let utyp, ubody =
-      (* allow_deferred case *)
-      if not poly &&
-         (keep_body_ucst_separate
-          || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
-      then make_univs_deferred ~initial_euctx ~poly ~uctx ~udecl t b
-      (* private_poly_univs case *)
-      else if poly && opaque && private_poly_univs ()
-      then make_univs_private_poly ~poly ~uctx ~udecl t b
-      else make_univs ~poly ~uctx ~udecl t b
-    in
-    definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
-  in
-  let entries = CList.map make_entry elist  in
-  { name; entries; uctx }
-
 type 'a constant_entry =
   | DefinitionEntry of 'a proof_entry
   | ParameterEntry of Entries.parameter_entry
@@ -271,7 +125,7 @@ type 'a constant_entry =
 
 type constant_obj = {
   cst_kind : Decls.logical_kind;
-  cst_locl : import_status;
+  cst_locl : Locality.import_status;
 }
 
 let load_constant i ((sp,kn), obj) =
@@ -285,8 +139,8 @@ let load_constant i ((sp,kn), obj) =
 let open_constant f i ((sp,kn), obj) =
   (* Never open a local definition *)
   match obj.cst_locl with
-  | ImportNeedQualified -> ()
-  | ImportDefaultBehavior ->
+  | Locality.ImportNeedQualified -> ()
+  | Locality.ImportDefaultBehavior ->
     let con = Global.constant_of_delta_kn kn in
     if Libobject.in_filter_ref (GlobRef.ConstRef con) f then
       Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con)
@@ -340,7 +194,7 @@ let register_constant kn kind local =
   update_tables kn
 
 let register_side_effect (c, role) =
-  let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in
+  let () = register_constant c Decls.(IsProof Theorem) Locality.ImportDefaultBehavior in
   match role with
   | None -> ()
   | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|]
@@ -497,14 +351,14 @@ let define_constant ~name cd =
   if unsafe || is_unsafe_typing_flags() then feedback_axiom();
   kn
 
-let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
+let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind cd =
   let () = check_exists name in
   let kn = define_constant ~name cd in
   (* Register the libobjects attached to the constants *)
   let () = register_constant kn kind local in
   kn
 
-let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de =
+let declare_private_constant ?role ?(local = Locality.ImportDefaultBehavior) ~name ~kind de =
   let kn, eff =
     let de =
       if not de.proof_entry_opaque then
@@ -684,180 +538,6 @@ module Internal = struct
   let objConstant = objConstant
 
 end
-(*** Proof Global Environment ***)
-
-type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
-
-let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
-  let { section_vars; proof; udecl; initial_euctx } = ps in
-  let { Proof.name; poly; entry; sigma } = Proof.data proof in
-
-  (* We don't allow poly = true in this path *)
-  if poly then
-    CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants.");
-
-  let fpl, uctx = Future.split2 fpl in
-  (* Because of dependent subgoals at the beginning of proofs, we could
-     have existential variables in the initial types of goals, we need to
-     normalise them for the kernel. *)
-  let subst_evar k = Evd.existential_opt_value0 sigma k in
-  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst initial_euctx) in
-
-  (* We only support opaque proofs, this will be enforced by using
-     different entries soon *)
-  let opaque = true in
-  let make_entry p (_, types) =
-    (* Already checked the univ_decl for the type universes when starting the proof. *)
-    let univs = UState.univ_entry ~poly:false initial_euctx in
-    let types = nf (EConstr.Unsafe.to_constr types) in
-
-    Future.chain p (fun (pt,eff) ->
-        (* Deferred proof, we already checked the universe declaration with
-             the initial universes, ensure that the final universes respect
-             the declaration as well. If the declaration is non-extensible,
-             this will prevent the body from adding universes and constraints. *)
-        let uctx = Future.force uctx in
-        let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
-        let used_univs = Univ.LSet.union
-            (Vars.universes_of_constr types)
-            (Vars.universes_of_constr pt)
-        in
-        let univs = UState.restrict uctx used_univs in
-        let univs = UState.check_mono_univ_decl univs udecl in
-        (pt,univs),eff)
-    |> delayed_definition_entry ~opaque ~feedback_id ~section_vars ~univs ~types
-  in
-  let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
-  { name; entries; uctx = initial_euctx }
-
-let close_future_proof = close_proof_delayed
-
-let return_partial_proof { proof } =
- let proofs = Proof.partial_proof proof in
- let Proof.{sigma=evd} = Proof.data proof in
- let eff = Evd.eval_side_effects evd in
- (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
-     side-effects... This may explain why one need to uniquize side-effects
-     thereafter... *)
- let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
- proofs, Evd.evar_universe_context evd
-
-let return_proof ps =
-  let p, uctx = prepare_proof ~unsafe_typ:false ps in
-  List.map (fun (((_ub, body),eff),_) -> (body,eff)) p, uctx
-
-let update_global_env =
-  map_proof (fun p ->
-      let { Proof.sigma } = Proof.data p in
-      let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
-      let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in
-      p)
-
-let next = let n = ref 0 in fun () -> incr n; !n
-
-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 goals = [ (Global.env_of_context sign , typ) ] in
-  let pf = start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
-  let pf, status = by tac pf in
-  let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in
-  match entries with
-  | [entry] ->
-    entry, status, uctx
-  | _ ->
-    CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
-
-let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
-  let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
-  let sign = Environ.(val_of_named_context (named_context env)) in
-  let ce, status, uctx = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
-  let cb, uctx =
-    if side_eff then inline_private_constants ~uctx env ce
-    else
-      (* GG: side effects won't get reset: no need to treat their universes specially *)
-      let (cb, ctx), _eff = Future.force ce.proof_entry_body in
-      cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx
-  in
-  cb, ce.proof_entry_type, ce.proof_entry_universes, status, uctx
-
-let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl =
-  (* EJGA: flush_and_check_evars is only used in abstract, could we
-     use a different API? *)
-  let concl =
-    try Evarutil.flush_and_check_evars sigma concl
-    with Evarutil.Uninstantiated_evar _ ->
-      CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.")
-  in
-  let sigma, concl =
-    (* FIXME: should be done only if the tactic succeeds *)
-    let sigma = Evd.minimize_universes sigma in
-    sigma, Evarutil.nf_evars_universes sigma concl
-  in
-  let concl = EConstr.of_constr concl in
-  let uctx = Evd.evar_universe_context sigma in
-  let (const, safe, uctx) =
-    try build_constant_by_tactic ~name ~opaque:Transparent ~poly ~uctx ~sign:secsign concl solve_tac
-    with Logic_monad.TacticFailure e as src ->
-    (* if the tactic [tac] fails, it reports a [TacticFailure e],
-       which is an error irrelevant to the proof system (in fact it
-       means that [e] comes from [tac] failing to yield enough
-       success). Hence it reraises [e]. *)
-    let (_, info) = Exninfo.capture src in
-    Exninfo.iraise (e, info)
-  in
-  let sigma = Evd.set_universe_context sigma uctx in
-  let body, effs = Future.force const.proof_entry_body in
-  (* We drop the side-effects from the entry, they already exist in the ambient environment *)
-  let const = Internal.map_entry_body const ~f:(fun _ -> body, ()) in
-  (* EJGA: Hack related to the above call to
-     `build_constant_by_tactic` with `~opaque:Transparent`. Even if
-     the abstracted term is destined to be opaque, if we trigger the
-     `if poly && opaque && private_poly_univs ()` in `Proof_global`
-     kernel will boom. This deserves more investigation. *)
-  let const = Internal.set_opacity ~opaque const in
-  let const, args = Internal.shrink_entry sign const in
-  let cst () =
-    (* do not compute the implicit arguments, it may be costly *)
-    let () = Impargs.make_implicit_args false in
-    (* ppedrot: seems legit to have abstracted subproofs as local*)
-    declare_private_constant ~local:ImportNeedQualified ~name ~kind const
-  in
-  let cst, eff = Impargs.with_implicit_protection cst () in
-  let inst = match const.proof_entry_universes with
-  | Entries.Monomorphic_entry _ -> EConstr.EInstance.empty
-  | Entries.Polymorphic_entry (_, ctx) ->
-    (* We mimic what the kernel does, that is ensuring that no additional
-       constraints appear in the body of polymorphic constants. Ideally this
-       should be enforced statically. *)
-    let (_, body_uctx), _ = Future.force const.proof_entry_body in
-    let () = assert (Univ.ContextSet.is_empty body_uctx) in
-    EConstr.EInstance.make (Univ.UContext.instance ctx)
-  in
-  let args = List.map EConstr.of_constr args in
-  let lem = EConstr.mkConstU (cst, inst) in
-  let effs = Evd.concat_side_effects eff effs in
-  effs, sigma, lem, args, safe
-
-let get_goal_context pf i =
-  let p = get_proof pf in
-  Proof.get_goal_context_gen p i
-
-let get_current_goal_context pf =
-  let p = get_proof pf in
-  try Proof.get_goal_context_gen p 1
-  with
-  | Proof.NoSuchGoal _ ->
-    (* spiwack: returning empty evar_map, since if there is no goal,
-       under focus, there is no accessible evar either. EJGA: this
-       seems strange, as we have pf *)
-    let env = Global.env () in
-    Evd.from_env env, env
-
-let get_current_context pf =
-  let p = get_proof pf in
-  Proof.get_proof_context p
 
 let declare_definition_scheme ~internal ~univs ~role ~name c =
   let kind = Decls.(IsDefinition Scheme) in
@@ -866,38 +546,6 @@ let declare_definition_scheme ~internal ~univs ~role ~name c =
   let () = if internal then () else definition_message name in
   kn, eff
 
-let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme
-let _ = Abstract.declare_abstract := declare_abstract
-
-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 =
@@ -907,11 +555,11 @@ let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
   in
   let ubind = UState.universe_binders uctx in
   let dref = match scope with
-  | Discharge ->
+  | Locality.Discharge ->
     let () = declare_variable_core ~name ~kind (SectionLocalDef entry) in
     if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
     Names.GlobRef.VarRef name
-  | Global local ->
+  | Locality.Global local ->
     let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in
     let gr = Names.GlobRef.ConstRef kn in
     if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
@@ -920,7 +568,7 @@ let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
   in
   let () = Impargs.maybe_declare_manual_implicits false dref impargs in
   let () = definition_message name in
-  Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook;
+  Hook.call ?hook { Hook.S.uctx; obls; scope; dref };
   dref
 
 let declare_entry = declare_entry_core ~obls:[]
@@ -938,22 +586,10 @@ 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 declare_mutually_recursive_core ~info ~cinfo ~opaque ~ntns ~uctx ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) () =
+  let { Info.poly; udecl; scope; kind; _ } = info in
   let vars, fixdecls, indexes =
-    mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
+    mutual_make_bodies ~fixitems:cinfo ~rec_declaration ~possible_indexes in
   let uctx, univs =
     (* XXX: Obligations don't do this, this seems like a bug? *)
     if restrict_ucontext
@@ -966,18 +602,18 @@ let declare_mutually_recursive_core ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntn
       uctx, univs
   in
   let csts = CList.map2
-      (fun Recthm.{ name; typ; impargs } body ->
+      (fun CInfo.{ name; typ; impargs } body ->
          let entry = definition_entry ~opaque ~types:typ ~univs body in
          declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
-      fixitems fixdecls
+      cinfo fixdecls
   in
   let isfix = Option.has_some possible_indexes in
-  let fixnames = List.map (fun { Recthm.name } -> name) fixitems in
+  let fixnames = List.map (fun { CInfo.name } -> name) cinfo in
   recursive_message isfix indexes fixnames;
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   csts
 
-let declare_mutually_recursive = declare_mutually_recursive_core ~restrict_ucontext:true
+let declare_mutually_recursive = declare_mutually_recursive_core ~restrict_ucontext:true ()
 
 let warn_let_as_axiom =
   CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
@@ -986,8 +622,8 @@ let warn_let_as_axiom =
 
 let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
   let local = match scope with
-    | Discharge -> warn_let_as_axiom name; ImportNeedQualified
-    | Global local -> local
+    | Locality.Discharge -> warn_let_as_axiom name; Locality.ImportNeedQualified
+    | Locality.Global local -> local
   in
   let kind = Decls.(IsAssumption Conjectural) in
   let decl = ParameterEntry pe in
@@ -1001,20 +637,22 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
 
 (* Preparing proof entries *)
 
-let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma =
+let prepare_definition ~info ~opaque ~body ~typ sigma =
+  let { Info.poly; udecl; inline; _ } = info in
   let env = Global.env () in
   Pretyping.check_evars_are_solved ~program_mode:false env sigma;
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true
-      sigma (fun nf -> nf body, Option.map nf types)
+      sigma (fun nf -> nf body, Option.map nf typ)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
-  let entry = definition_entry ?opaque ?inline ?types ~univs body in
+  let entry = definition_entry ~opaque ~inline ?types ~univs body in
   let uctx = Evd.evar_universe_context sigma in
   entry, uctx
 
-let declare_definition_core ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
-    ~obls ~poly ?inline ~types ~body sigma =
-  let entry, uctx = prepare_definition ~opaque ~poly ~udecl ~types ~body ?inline sigma in
+let declare_definition_core ~info ~cinfo ~opaque ~obls ~body sigma =
+  let { CInfo.name; impargs; typ; _ } = cinfo in
+  let entry, uctx = prepare_definition ~info ~opaque ~body ~typ sigma in
+  let { Info.scope; kind; hook; _ } = info in
   declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry
 
 let declare_definition = declare_definition_core ~obls:[]
@@ -1043,10 +681,17 @@ let prepare_parameter ~poly ~udecl ~types sigma =
   let univs = Evd.check_univ_decl ~poly sigma udecl in
   sigma, (None(*proof using*), (typ, univs), None(*inline*))
 
-(* Compat: will remove *)
-exception AlreadyDeclared = DeclareUniv.AlreadyDeclared
+type progress = Remain of int | Dependent | Defined of GlobRef.t
 
-module Obls = struct
+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 Obls_ = struct
 
 open Constr
 
@@ -1070,37 +715,32 @@ type obligations = {obls : Obligation.t array; remaining : int}
 type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint
 
 module ProgramDecl = struct
+
   type t =
-    { prg_name : Id.t
+    { prg_cinfo : constr CInfo.t
+    ; prg_info : Info.t
+    ; prg_opaque : bool
     ; prg_body : constr
-    ; prg_type : constr
-    ; prg_ctx : UState.t
-    ; prg_univdecl : UState.universe_decl
+    ; prg_uctx : UState.t
     ; prg_obligations : obligations
     ; prg_deps : Id.t list
     ; prg_fixkind : fixpoint_kind option
-    ; prg_implicits : Impargs.manual_implicits
     ; prg_notations : Vernacexpr.decl_notation list
-    ; prg_poly : bool
-    ; prg_scope : locality
-    ; prg_kind : Decls.definition_object_kind
     ; prg_reduce : constr -> constr
-    ; prg_hook : Hook.t option
-    ; prg_opaque : bool }
+    }
 
   open Obligation
 
-  let make ?(opaque = false) ?hook n ~udecl ~uctx ~impargs ~poly ~scope ~kind b
-      t deps fixkind notations obls reduce =
-    let obls', b =
-      match b with
+  let make ~info ~cinfo ~opaque ~ntns ~reduce ~deps ~uctx ~body ~fixpoint_kind obls =
+    let obls', body =
+      match body with
       | None ->
         assert (Int.equal (Array.length obls) 0);
-        let n = Nameops.add_suffix n "_obligation" in
+        let n = Nameops.add_suffix cinfo.CInfo.name "_obligation" in
         ( [| { obl_name = n
              ; obl_body = None
              ; obl_location = Loc.tag Evar_kinds.InternalHole
-             ; obl_type = t
+             ; obl_type = cinfo.CInfo.typ
              ; obl_status = (false, Evar_kinds.Expand)
              ; obl_deps = Int.Set.empty
              ; obl_tac = None } |]
@@ -1118,25 +758,34 @@ module ProgramDecl = struct
             obls
         , b )
     in
-    let ctx = UState.make_flexible_nonalgebraic uctx in
-    { prg_name = n
-    ; prg_body = b
-    ; prg_type = reduce t
-    ; prg_ctx = ctx
-    ; prg_univdecl = udecl
+    let prg_uctx = UState.make_flexible_nonalgebraic uctx in
+    { prg_cinfo = { cinfo with CInfo.typ = reduce cinfo.CInfo.typ }
+    ; prg_info = info
+    ; prg_opaque = opaque
+    ; prg_body = body
+    ; prg_uctx
     ; prg_obligations = {obls = obls'; remaining = Array.length obls'}
     ; prg_deps = deps
-    ; prg_fixkind = fixkind
-    ; prg_notations = notations
-    ; prg_implicits = impargs
-    ; prg_poly = poly
-    ; prg_scope = scope
-    ; prg_kind = kind
-    ; prg_reduce = reduce
-    ; prg_hook = hook
-    ; prg_opaque = opaque }
-
-  let set_uctx ~uctx prg = {prg with prg_ctx = uctx}
+    ; prg_fixkind = fixpoint_kind
+    ; prg_notations = ntns
+    ; prg_reduce = reduce }
+
+  let show prg =
+    let { CInfo.name; typ; _ } = prg.prg_cinfo in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    Id.print name ++ spc () ++ str ":" ++ spc ()
+    ++ Printer.pr_constr_env env sigma typ
+    ++ spc () ++ str ":=" ++ fnl ()
+    ++ Printer.pr_constr_env env sigma prg.prg_body
+
+  module Internal = struct
+    let get_name prg = prg.prg_cinfo.CInfo.name
+    let get_uctx prg = prg.prg_uctx
+    let set_uctx ~uctx prg = {prg with prg_uctx = uctx}
+    let get_poly prg = prg.prg_info.Info.poly
+    let get_obligations prg = prg.prg_obligations
+  end
 end
 
 open Obligation
@@ -1213,7 +862,7 @@ let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
 
 let add_hint local prg cst =
   let locality = if local then Goptions.OptLocal else Goptions.OptExport in
-  Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst)
+  Hints.add_hints ~locality [Id.to_string prg.prg_cinfo.CInfo.name] (unfold_entry cst)
 
 (* true = hide obligations *)
 let get_hide_obligations =
@@ -1223,14 +872,16 @@ let get_hide_obligations =
     ~value:false
 
 let declare_obligation prg obl ~uctx ~types ~body =
-  let univs = UState.univ_entry ~poly:prg.prg_poly uctx in
+  let poly = prg.prg_info.Info.poly in
+  let univs = UState.univ_entry ~poly uctx in
   let body = prg.prg_reduce body in
   let types = Option.map prg.prg_reduce types in
   match obl.obl_status with
-  | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)})
+  | _, Evar_kinds.Expand ->
+    (false, {obl with obl_body = Some (TermObl body)}, [])
   | force, Evar_kinds.Define opaque ->
     let opaque = (not force) && opaque in
-    let poly = prg.prg_poly in
+    let poly = prg.prg_info.Info.poly in
     let ctx, body, ty, args =
       if not poly then shrink_body body types
       else ([], body, types, [||])
@@ -1239,7 +890,7 @@ let declare_obligation prg obl ~uctx ~types ~body =
     (* ppedrot: seems legit to have obligations as local *)
     let constant =
       declare_constant ~name:obl.obl_name
-        ~local:ImportNeedQualified
+        ~local:Locality.ImportNeedQualified
         ~kind:Decls.(IsProof Property)
         (DefinitionEntry ce)
     in
@@ -1257,7 +908,7 @@ let declare_obligation prg obl ~uctx ~types ~body =
                 (mkApp (mkConst constant, args))
                 ctx))
     in
-    (true, {obl with obl_body = body})
+    (true, {obl with obl_body = body}, [GlobRef.ConstRef constant])
 
 (* Updating the obligation meta-info on close *)
 
@@ -1323,7 +974,6 @@ module State = struct
   let prg_ref, prg_tag =
     Summary.ref_tag ProgMap.empty ~name:"program-tcc-table"
 
-  let num_pending () = num_pending !prg_ref
   let first_pending () = first_pending !prg_ref
   let get_unique_open_prog id = get_unique_open_prog !prg_ref id
   let add id prg = prg_ref := add !prg_ref id prg
@@ -1349,8 +999,8 @@ let check_solved_obligations ~what_for : unit =
         ++ str "unsolved obligations" )
 
 let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
-let progmap_remove pm prg = ProgMap.remove prg.prg_name pm
-let progmap_replace prg' pm = map_replace prg'.prg_name prg' pm
+let progmap_remove pm prg = ProgMap.remove prg.prg_cinfo.CInfo.name pm
+let progmap_replace prg' pm = map_replace prg'.prg_cinfo.CInfo.name prg' pm
 let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0
 
 let obligations_message rem =
@@ -1359,8 +1009,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
@@ -1430,33 +1078,22 @@ let replace_appvars subst =
 let subst_prog subst prg =
   if get_hide_obligations () then
     ( replace_appvars subst prg.prg_body
-    , replace_appvars subst (* Termops.refresh_universes *) prg.prg_type )
+    , replace_appvars subst (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
   else
     let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in
     ( Vars.replace_vars subst' prg.prg_body
-    , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type )
+    , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
 
 let declare_definition prg =
   let varsubst = obligation_substitution true prg in
-  let sigma = Evd.from_ctx prg.prg_ctx in
+  let sigma = Evd.from_ctx prg.prg_uctx in
   let body, types = subst_prog varsubst prg in
   let body, types = EConstr.(of_constr body, Some (of_constr types)) in
-  (* All these should be grouped into a struct a some point *)
-  let opaque, poly, udecl, hook =
-    (prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook)
-  in
-  let name, scope, kind, impargs =
-    ( prg.prg_name
-    , prg.prg_scope
-    , Decls.(IsDefinition prg.prg_kind)
-    , prg.prg_implicits )
-  in
+  let cinfo = { prg.prg_cinfo with CInfo.typ = types } in
+  let name, info, opaque = prg.prg_cinfo.CInfo.name, prg.prg_info, prg.prg_opaque in
   let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
   (* XXX: This is doing normalization twice *)
-  let kn =
-    declare_definition_core ~name ~scope ~kind ~impargs ?hook ~obls
-      ~opaque ~poly ~udecl ~types ~body sigma
-  in
+  let kn = declare_definition_core ~cinfo ~info ~obls ~body ~opaque sigma in
   let pm = progmap_remove !State.prg_ref prg in
   State.prg_ref := pm;
   kn
@@ -1487,7 +1124,7 @@ let declare_mutual_definition l =
     let oblsubst = obligation_substitution true x in
     let subs, typ = subst_prog oblsubst x in
     let env = Global.env () in
-    let sigma = Evd.from_ctx x.prg_ctx in
+    let sigma = Evd.from_ctx x.prg_uctx in
     let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in
     let term =
       snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs))
@@ -1497,7 +1134,7 @@ let declare_mutual_definition l =
     in
     let term = EConstr.to_constr sigma term in
     let typ = EConstr.to_constr sigma typ in
-    let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in
+    let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs) in
     let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in
     (def, oblsubst)
   in
@@ -1515,13 +1152,13 @@ let declare_mutual_definition l =
         ( d :: a1
         , r :: a2
         , typ :: a3
-        , Recthm.{name; typ; impargs; args = []} :: a4 ))
+        , CInfo.{name; typ; impargs; args = []} :: a4 ))
       defs first.prg_deps ([], [], [], [])
   in
   let fixkind = Option.get first.prg_fixkind in
   let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in
   let rvec = Array.of_list fixrs in
-  let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in
+  let namevec = Array.of_list (List.map (fun x -> Name x.prg_cinfo.CInfo.name) l) in
   let rec_declaration = (Array.map2 Context.make_annot namevec rvec, arrrec, recvec) in
   let possible_indexes =
     match fixkind with
@@ -1530,24 +1167,22 @@ let declare_mutual_definition l =
     | IsCoFixpoint -> None
   in
   (* In the future we will pack all this in a proper record *)
-  let poly, scope, ntns, opaque =
-    (first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque)
-  in
-  let kind =
+  (* XXX: info refactoring *)
+  let _kind =
     if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint)
     else Decls.(IsDefinition CoFixpoint)
   in
+  let scope = first.prg_info.Info.scope in
   (* Declare the recursive definitions *)
-  let udecl = UState.default_univ_decl in
   let kns =
-    declare_mutually_recursive_core ~scope ~opaque ~kind ~udecl ~ntns
-      ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly
-      ~restrict_ucontext:false fixitems
+    declare_mutually_recursive_core ~info:first.prg_info ~ntns:first.prg_notations
+      ~uctx:first.prg_uctx ~rec_declaration ~possible_indexes ~opaque:first.prg_opaque
+      ~restrict_ucontext:false ~cinfo:fixitems ()
   in
   (* Only for the first constant *)
   let dref = List.hd kns in
   Hook.(
-    call ?hook:first.prg_hook {S.uctx = first.prg_ctx; obls; scope; dref});
+    call ?hook:first.prg_info.Info.hook {S.uctx = first.prg_uctx; obls; scope; dref});
   let pm = List.fold_left progmap_remove !State.prg_ref l in
   State.prg_ref := pm;
   dref
@@ -1587,74 +1222,60 @@ let dependencies obls n =
 let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto =
   let obls = Array.copy obls in
   let () = obls.(num) <- obl in
-  let prg = {prg with prg_ctx = uctx} in
+  let prg = {prg with prg_uctx = uctx} in
   let _progress = update_obls prg obls (pred rem) in
   let () =
     if pred rem > 0 then
       let deps = dependencies obls num in
       if not (Int.Set.is_empty deps) then
-        let _progress = auto (Some prg.prg_name) deps None in
+        let _progress = auto (Some prg.prg_cinfo.CInfo.name) deps None in
         ()
       else ()
     else ()
   in
   ()
 
-type obligation_resolver =
-     Id.t option
-  -> Int.Set.t
-  -> unit Proofview.tactic option
-  -> progress
-
-type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver}
-
-let obligation_terminator entries uctx {name; num; auto} =
-  match entries with
-  | [entry] ->
-    let env = Global.env () in
-    let ty = entry.proof_entry_type in
-    let body, uctx = inline_private_constants ~uctx env entry in
-    let sigma = Evd.from_ctx uctx in
-    Inductiveops.control_only_guard (Global.env ()) sigma
-      (EConstr.of_constr body);
-    (* Declare the obligation ourselves and drop the hook *)
-    let prg = Option.get (State.find name) in
-    let {obls; remaining = rem} = prg.prg_obligations in
-    let obl = obls.(num) in
-    let status =
-      match (obl.obl_status, entry.proof_entry_opaque) with
-      | (_, Evar_kinds.Expand), true -> err_not_transp ()
-      | (true, _), true -> err_not_transp ()
-      | (false, _), true -> Evar_kinds.Define true
-      | (_, Evar_kinds.Define true), false -> Evar_kinds.Define false
-      | (_, status), false -> status
-    in
-    let obl = {obl with obl_status = (false, status)} in
-    let uctx = if prg.prg_poly then uctx else UState.union prg.prg_ctx uctx in
-    let defined, obl = declare_obligation prg obl ~body ~types:ty ~uctx in
-    let prg_ctx =
-      if prg.prg_poly then
-        (* Polymorphic *)
-        (* We merge the new universes and constraints of the
-           polymorphic obligation with the existing ones *)
-        UState.union prg.prg_ctx uctx
-      else if
-        (* The first obligation, if defined,
-           declares the univs of the constant,
-           each subsequent obligation declares its own additional
-           universes and constraints if any *)
-        defined
-      then
-        UState.from_env (Global.env ())
-      else uctx
-    in
-    update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto
-  | _ ->
-    CErrors.anomaly
-      Pp.(
-        str
-          "[obligation_terminator] close_proof returned more than one proof \
-           term")
+let obligation_terminator ~entry ~uctx ~oinfo:{name; num; auto} =
+  let env = Global.env () in
+  let ty = entry.proof_entry_type in
+  let body, uctx = inline_private_constants ~uctx env entry in
+  let sigma = Evd.from_ctx uctx in
+  Inductiveops.control_only_guard (Global.env ()) sigma
+    (EConstr.of_constr body);
+  (* Declare the obligation ourselves and drop the hook *)
+  let prg = Option.get (State.find name) in
+  let {obls; remaining = rem} = prg.prg_obligations in
+  let obl = obls.(num) in
+  let status =
+    match (obl.obl_status, entry.proof_entry_opaque) with
+    | (_, Evar_kinds.Expand), true -> err_not_transp ()
+    | (true, _), true -> err_not_transp ()
+    | (false, _), true -> Evar_kinds.Define true
+    | (_, Evar_kinds.Define true), false -> Evar_kinds.Define false
+    | (_, status), false -> status
+  in
+  let obl = {obl with obl_status = (false, status)} in
+  let poly = prg.prg_info.Info.poly in
+  let uctx = if poly then uctx else UState.union prg.prg_uctx uctx in
+  let defined, obl, cst = declare_obligation prg obl ~body ~types:ty ~uctx in
+  let prg_ctx =
+    if poly then
+      (* Polymorphic *)
+      (* We merge the new universes and constraints of the
+         polymorphic obligation with the existing ones *)
+      UState.union prg.prg_uctx uctx
+    else if
+      (* The first obligation, if defined,
+         declares the univs of the constant,
+         each subsequent obligation declares its own additional
+         universes and constraints if any *)
+      defined
+    then
+      UState.from_env (Global.env ())
+    else uctx
+  in
+  update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto;
+  cst
 
 (* Similar to the terminator but for the admitted path; this assumes
    the admitted constant was already declared.
@@ -1674,7 +1295,7 @@ let obligation_admitted_terminator {name; num; auto} ctx' dref =
     | _ -> ()
   in
   let inst, ctx' =
-    if not prg.prg_poly (* Not polymorphic *) then
+    if not prg.prg_info.Info.poly (* Not polymorphic *) then
       (* The universe context was declared globally, we continue
          from the new global environment. *)
       let ctx = UState.from_env (Global.env ()) in
@@ -1692,16 +1313,16 @@ let obligation_admitted_terminator {name; num; auto} ctx' dref =
 end
 
 (************************************************************************)
-(* Commom constant saving path, for both Qed and Admitted               *)
+(* Handling of interactive proofs                                       *)
 (************************************************************************)
 
-(* Support for mutually proved theorems *)
+type lemma_possible_guards = int list list
 
 module Proof_ending = struct
 
   type t =
     | Regular
-    | End_obligation of Obls.obligation_qed_info
+    | 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
@@ -1712,58 +1333,533 @@ module Proof_ending = struct
 
 end
 
-type lemma_possible_guards = int list list
+(* Alias *)
+module Proof_ = Proof
+module Proof = struct
 
-module Info = struct
+module Proof_info = struct
 
   type t =
-    { hook : Hook.t option
+    { cinfo : Constr.t CInfo.t list
+    (** cinfo contains each individual constant info in a mutual decl *)
+    ; info : Info.t
     ; 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
+    (** thms and compute guard are specific only to
+       start_lemma_with_initialization + regular terminator, so we
+       could make this per-proof kind *)
     }
 
-  let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Global ImportDefaultBehavior)
-      ?(kind=Decls.(IsProof Lemma)) ?(compute_guard=[]) ?(thms=[]) () =
-    { hook
+  let make ~cinfo ~info ?(compute_guard=[]) ?(proof_ending=Proof_ending.Regular) () =
+    { cinfo
+    ; info
     ; 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 }
+  let add_first_thm ~pinfo ~name ~typ ~impargs =
+    let cinfo : Constr.t CInfo.t = CInfo.make ~name ~impargs ~typ:(EConstr.Unsafe.to_constr typ) () in
+    { pinfo with cinfo = cinfo :: pinfo.cinfo }
 
+  (* This is called by the STM, and we have to fixup cinfo later as
+     indeed it will not be correct *)
+  let default () = make ~cinfo:[] ~info:(Info.make ()) ()
 end
 
+type t =
+  { endline_tactic : Genarg.glob_generic_argument option
+  ; section_vars : Id.Set.t option
+  ; proof : Proof.t
+  ; initial_euctx : UState.t
+  (** The initial universe context (for the statement) *)
+  ; pinfo : Proof_info.t
+  }
+
+(*** Proof Global manipulation ***)
+
+let info { pinfo } = pinfo
+let get ps = ps.proof
+let get_name ps = (Proof.data ps.proof).Proof.name
+let get_initial_euctx ps = ps.initial_euctx
+
+let fold ~f p = f p.proof
+let map ~f p = { p with proof = f p.proof }
+let map_fold ~f p = let proof, res = f p.proof in { p with proof }, res
+
+let map_fold_endline ~f ps =
+  let et =
+    match ps.endline_tactic with
+    | None -> Proofview.tclUNIT ()
+    | Some tac ->
+      let open Geninterp in
+      let {Proof.poly} = Proof.data ps.proof in
+      let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in
+      let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
+      let tac = Geninterp.interp tag ist tac in
+      Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
+  in
+  let (newpr,ret) = f et ps.proof in
+  let ps = { ps with proof = newpr } in
+  ps, ret
+
+let compact pf = map ~f:Proof.compact pf
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+let set_endline_tactic tac ps =
+  { ps with endline_tactic = Some tac }
+
+let initialize_named_context_for_proof () =
+  let sign = Global.named_context () in
+  List.fold_right
+    (fun d signv ->
+      let id = NamedDecl.get_id d in
+      let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in
+      Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
+
+let start_proof_core ~name ~typ ~pinfo ?(sign=initialize_named_context_for_proof ()) sigma =
+  (* 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
+     program_inference_hook *)
+  let { Proof_info.info = { Info.poly; _ }; _ } = pinfo in
+  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
+  { proof
+  ; endline_tactic = None
+  ; section_vars = None
+  ; initial_euctx
+  ; pinfo
+  }
+
+(** [start_proof ~info ~cinfo sigma] starts a proof of [cinfo].
+   The proof is started in the evar map [sigma] (which
+   can typically contain universe constraints) *)
+let start_core ~info ~cinfo ?proof_ending sigma =
+  let { CInfo.name; typ; _ } = cinfo in
+  let cinfo = [{ cinfo with CInfo.typ = EConstr.Unsafe.to_constr cinfo.CInfo.typ }] in
+  let pinfo = Proof_info.make ~cinfo ~info ?proof_ending () in
+  start_proof_core ~name ~typ ~pinfo ?sign:None sigma
+
+let start = start_core ?proof_ending:None
+
+let start_dependent ~info ~name ~proof_ending goals =
+  let proof = Proof.dependent_start ~name ~poly:info.Info.poly goals in
+  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+  let cinfo = [] in
+  let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in
+  { proof
+  ; endline_tactic = None
+  ; section_vars = None
+  ; initial_euctx
+  ; pinfo
+  }
+
+let start_derive ~f ~name ~info goals =
+  let proof_ending = Proof_ending.End_derive {f; name} in
+  start_dependent ~info ~name ~proof_ending goals
+
+let start_equations ~name ~info ~hook ~types sigma goals =
+  let proof_ending = Proof_ending.End_equations {hook; i=name; types; sigma} in
+  start_dependent ~name ~info ~proof_ending goals
+
+let rec_tac_initializer finite guard thms snl =
+  if finite then
+    match List.map (fun { CInfo.name; typ } -> name, (EConstr.of_constr typ)) thms with
+    | (id,_)::l -> Tactics.mutual_cofix id l 0
+    | _ -> assert false
+  else
+    (* nl is dummy: it will be recomputed at Qed-time *)
+    let nl = match snl with
+     | None -> List.map succ (List.map List.last guard)
+     | Some nl -> nl
+    in match List.map2 (fun { CInfo.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with
+       | (id,n,_)::l -> Tactics.mutual_fix id n l 0
+       | _ -> assert false
+
+let start_with_initialization ~info ~cinfo sigma =
+  let { CInfo.name; typ; args } = cinfo in
+  let init_tac = Tactics.auto_intros_tac args in
+  let pinfo = Proof_info.make ~cinfo:[cinfo] ~info () in
+  let lemma = start_proof_core ~name ~typ:(EConstr.of_constr typ) ~pinfo ?sign:None sigma in
+  map lemma ~f:(fun p ->
+      pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)
+
+type mutual_info = (bool * lemma_possible_guards * Constr.t option list option)
+
+let start_mutual_with_initialization ~info ~cinfo ~mutual_info sigma snl =
+  let intro_tac { CInfo.args; _ } = Tactics.auto_intros_tac args in
+  let init_tac, compute_guard =
+    let (finite,guard,init_terms) = mutual_info in
+    let rec_tac = rec_tac_initializer finite guard cinfo snl in
+    let term_tac =
+      match init_terms with
+      | None ->
+        List.map intro_tac cinfo
+      | Some init_terms ->
+        (* This is the case for hybrid proof mode / definition
+           fixpoint, where terms for some constants are given with := *)
+        let tacl = List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) init_terms in
+        List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl cinfo
+    in
+    Tacticals.New.tclTHENS rec_tac term_tac, guard
+  in
+  match cinfo with
+  | [] -> CErrors.anomaly (Pp.str "No proof to start.")
+  | { CInfo.name; typ; impargs; _} :: thms ->
+    let pinfo = Proof_info.make ~cinfo ~info ~compute_guard () 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 typ = EConstr.of_constr typ in
+    let lemma = start_proof_core ~name ~typ ~pinfo sigma in
+    map lemma ~f:(fun p ->
+        pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)
+
+let get_used_variables pf = pf.section_vars
+let get_universe_decl pf = pf.pinfo.Proof_info.info.Info.udecl
+
+let set_used_variables ps l =
+  let open Context.Named.Declaration in
+  let env = Global.env () in
+  let ids = List.fold_right Id.Set.add l Id.Set.empty in
+  let ctx = Environ.keep_hyps env ids in
+  let ctx_set =
+    List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
+  let vars_of = Environ.global_vars_set in
+  let aux env entry (ctx, all_safe as orig) =
+    match entry with
+    | LocalAssum ({Context.binder_name=x},_) ->
+       if Id.Set.mem x all_safe then orig
+       else (ctx, all_safe)
+    | LocalDef ({Context.binder_name=x},bo, ty) as decl ->
+       if Id.Set.mem x all_safe then orig else
+       let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
+       if Id.Set.subset vars all_safe
+       then (decl :: ctx, Id.Set.add x all_safe)
+       else (ctx, all_safe) in
+  let ctx, _ =
+    Environ.fold_named_context aux env ~init:(ctx,ctx_set) in
+  if not (Option.is_empty ps.section_vars) then
+    CErrors.user_err Pp.(str "Used section variables can be declared only once");
+  ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) }
+
+let get_open_goals ps =
+  let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
+  List.length goals +
+  List.fold_left (+) 0
+    (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
+  List.length shelf
+
+type proof_object =
+  { name : Names.Id.t
+  (* [name] only used in the STM *)
+  ; entries : Evd.side_effects proof_entry list
+  ; uctx: UState.t
+  }
+
+let get_po_name { name } = name
+
+let private_poly_univs =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Private";"Polymorphic";"Universes"]
+    ~value:true
+
+(* XXX: This is still separate from close_proof below due to drop_pt in the STM *)
+(* XXX: Unsafe_typ:true is needed by vio files, see bf0499bc507d5a39c3d5e3bf1f69191339270729 *)
+let prepare_proof ~unsafe_typ { proof } =
+  let Proof.{name=pid;entry;poly} = Proof.data proof in
+  let initial_goals = Proofview.initial_goals entry in
+  let evd = Proof.return ~pid proof in
+  let eff = Evd.eval_side_effects evd in
+  let evd = Evd.minimize_universes evd in
+  let to_constr_body c =
+    match EConstr.to_constr_opt evd c with
+    | Some p ->
+      Vars.universes_of_constr p, p
+    | None ->
+      CErrors.user_err Pp.(str "Some unresolved existential variables remain")
+  in
+  let to_constr_typ t =
+    if unsafe_typ
+    then
+      let t = EConstr.Unsafe.to_constr t in
+      Vars.universes_of_constr t, t
+    else to_constr_body t
+  in
+  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+     side-effects... This may explain why one need to uniquize side-effects
+     thereafter... *)
+  (* EJGA: actually side-effects de-duplication and this codepath is
+     unrelated. Duplicated side-effects arise from incorrect scheme
+     generation code, the main bulk of it was mostly fixed by #9836
+     but duplication can still happen because of rewriting schemes I
+     think; however the code below is mostly untested, the only
+     code-paths that generate several proof entries are derive and
+     equations and so far there is no code in the CI that will
+     actually call those and do a side-effect, TTBOMK *)
+  (* EJGA: likely the right solution is to attach side effects to the first constant only? *)
+  let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in
+  proofs, Evd.evar_universe_context evd
+
+let make_univs_deferred ~poly ~initial_euctx ~uctx ~udecl
+    (used_univs_typ, typ) (used_univs_body, body) =
+  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+  let utyp = UState.univ_entry ~poly initial_euctx in
+  let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
+  (* For vi2vo compilation proofs are computed now but we need to
+     complement the univ constraints of the typ with the ones of
+     the body.  So we keep the two sets distinct. *)
+  let uctx_body = UState.restrict uctx used_univs in
+  let ubody = UState.check_mono_univ_decl uctx_body udecl in
+  utyp, ubody
+
+let make_univs_private_poly ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body) =
+  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+  let universes = UState.restrict uctx used_univs in
+  let typus = UState.restrict universes used_univs_typ in
+  let utyp = UState.check_univ_decl ~poly typus udecl in
+  let ubody = Univ.ContextSet.diff
+      (UState.context_set universes)
+      (UState.context_set typus)
+  in
+  utyp, ubody
+
+let make_univs ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body) =
+  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+  (* Since the proof is computed now, we can simply have 1 set of
+     constraints in which we merge the ones for the body and the ones
+     for the typ. We recheck the declaration after restricting with
+     the actually used universes.
+     TODO: check if restrict is really necessary now. *)
+  let ctx = UState.restrict uctx used_univs in
+  let utyp = UState.check_univ_decl ~poly ctx udecl in
+  utyp, Univ.ContextSet.empty
+
+let close_proof ~opaque ~keep_body_ucst_separate ps =
+
+  let { section_vars; proof; initial_euctx; pinfo } = ps in
+  let { Proof_info.info = { Info.udecl } } = pinfo in
+  let { Proof.name; poly } = Proof.data proof in
+  let unsafe_typ = keep_body_ucst_separate && not poly in
+  let elist, uctx = prepare_proof ~unsafe_typ ps in
+  let opaque = match opaque with
+    | Vernacexpr.Opaque -> true
+    | Vernacexpr.Transparent -> false in
+
+  let make_entry ((((_ub, body) as b), eff), ((_ut, typ) as t)) =
+    let utyp, ubody =
+      (* allow_deferred case *)
+      if not poly &&
+         (keep_body_ucst_separate
+          || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
+      then make_univs_deferred ~initial_euctx ~poly ~uctx ~udecl t b
+      (* private_poly_univs case *)
+      else if poly && opaque && private_poly_univs ()
+      then make_univs_private_poly ~poly ~uctx ~udecl t b
+      else make_univs ~poly ~uctx ~udecl t b
+    in
+    definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
+  in
+  let entries = CList.map make_entry elist  in
+  { name; entries; uctx }
+
+type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
+
+let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
+  let { section_vars; proof; initial_euctx; pinfo } = ps in
+  let { Proof_info.info = { Info.udecl } } = pinfo in
+  let { Proof.name; poly; entry; sigma } = Proof.data proof in
+
+  (* We don't allow poly = true in this path *)
+  if poly then
+    CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants.");
+
+  let fpl, uctx = Future.split2 fpl in
+  (* Because of dependent subgoals at the beginning of proofs, we could
+     have existential variables in the initial types of goals, we need to
+     normalise them for the kernel. *)
+  let subst_evar k = Evd.existential_opt_value0 sigma k in
+  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst initial_euctx) in
+
+  (* We only support opaque proofs, this will be enforced by using
+     different entries soon *)
+  let opaque = true in
+  let make_entry p (_, types) =
+    (* Already checked the univ_decl for the type universes when starting the proof. *)
+    let univs = UState.univ_entry ~poly:false initial_euctx in
+    let types = nf (EConstr.Unsafe.to_constr types) in
+
+    Future.chain p (fun (pt,eff) ->
+        (* Deferred proof, we already checked the universe declaration with
+             the initial universes, ensure that the final universes respect
+             the declaration as well. If the declaration is non-extensible,
+             this will prevent the body from adding universes and constraints. *)
+        let uctx = Future.force uctx in
+        let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
+        let used_univs = Univ.LSet.union
+            (Vars.universes_of_constr types)
+            (Vars.universes_of_constr pt)
+        in
+        let univs = UState.restrict uctx used_univs in
+        let univs = UState.check_mono_univ_decl univs udecl in
+        (pt,univs),eff)
+    |> delayed_definition_entry ~opaque ~feedback_id ~section_vars ~univs ~types
+  in
+  let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
+  { name; entries; uctx = initial_euctx }
+
+let close_future_proof = close_proof_delayed
+
+let return_partial_proof { proof } =
+ let proofs = Proof.partial_proof proof in
+ let Proof.{sigma=evd} = Proof.data proof in
+ let eff = Evd.eval_side_effects evd in
+ (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+     side-effects... This may explain why one need to uniquize side-effects
+     thereafter... *)
+ let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
+ proofs, Evd.evar_universe_context evd
+
+let return_proof ps =
+  let p, uctx = prepare_proof ~unsafe_typ:false ps in
+  List.map (fun (((_ub, body),eff),_) -> (body,eff)) p, uctx
+
+let update_global_env =
+  map ~f:(fun p ->
+      let { Proof.sigma } = Proof.data p in
+      let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
+      let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in
+      p)
+
+let next = let n = ref 0 in fun () -> incr n; !n
+
+let by tac = map_fold ~f:(Proof.solve (Goal_select.SelectNth 1) None tac)
+
+let build_constant_by_tactic ~name ?(opaque=Vernacexpr.Transparent) ~uctx ~sign ~poly (typ : EConstr.t) tac =
+  let evd = Evd.from_ctx uctx in
+  let typ_ = EConstr.Unsafe.to_constr typ in
+  let cinfo = [CInfo.make ~name ~typ:typ_ ()] in
+  let info = Info.make ~poly () in
+  let pinfo = Proof_info.make ~cinfo ~info () in
+  let pf = start_proof_core ~name ~typ ~pinfo ~sign evd in
+  let pf, status = by tac pf in
+  let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in
+  match entries with
+  | [entry] ->
+    entry, status, uctx
+  | _ ->
+    CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
+
+let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
+  let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
+  let sign = Environ.(val_of_named_context (named_context env)) in
+  let ce, status, uctx = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
+  let cb, uctx =
+    if side_eff then inline_private_constants ~uctx env ce
+    else
+      (* GG: side effects won't get reset: no need to treat their universes specially *)
+      let (cb, ctx), _eff = Future.force ce.proof_entry_body in
+      cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx
+  in
+  cb, ce.proof_entry_type, ce.proof_entry_universes, status, uctx
+
+let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl =
+  (* EJGA: flush_and_check_evars is only used in abstract, could we
+     use a different API? *)
+  let concl =
+    try Evarutil.flush_and_check_evars sigma concl
+    with Evarutil.Uninstantiated_evar _ ->
+      CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.")
+  in
+  let sigma, concl =
+    (* FIXME: should be done only if the tactic succeeds *)
+    let sigma = Evd.minimize_universes sigma in
+    sigma, Evarutil.nf_evars_universes sigma concl
+  in
+  let concl = EConstr.of_constr concl in
+  let uctx = Evd.evar_universe_context sigma in
+  let (const, safe, uctx) =
+    try build_constant_by_tactic ~name ~opaque:Vernacexpr.Transparent ~poly ~uctx ~sign:secsign concl solve_tac
+    with Logic_monad.TacticFailure e as src ->
+    (* if the tactic [tac] fails, it reports a [TacticFailure e],
+       which is an error irrelevant to the proof system (in fact it
+       means that [e] comes from [tac] failing to yield enough
+       success). Hence it reraises [e]. *)
+    let (_, info) = Exninfo.capture src in
+    Exninfo.iraise (e, info)
+  in
+  let sigma = Evd.set_universe_context sigma uctx in
+  let body, effs = Future.force const.proof_entry_body in
+  (* We drop the side-effects from the entry, they already exist in the ambient environment *)
+  let const = Internal.map_entry_body const ~f:(fun _ -> body, ()) in
+  (* EJGA: Hack related to the above call to
+     `build_constant_by_tactic` with `~opaque:Transparent`. Even if
+     the abstracted term is destined to be opaque, if we trigger the
+     `if poly && opaque && private_poly_univs ()` in `close_proof`
+     kernel will boom. This deserves more investigation. *)
+  let const = Internal.set_opacity ~opaque const in
+  let const, args = Internal.shrink_entry sign const in
+  let cst () =
+    (* do not compute the implicit arguments, it may be costly *)
+    let () = Impargs.make_implicit_args false in
+    (* ppedrot: seems legit to have abstracted subproofs as local*)
+    declare_private_constant ~local:Locality.ImportNeedQualified ~name ~kind const
+  in
+  let cst, eff = Impargs.with_implicit_protection cst () in
+  let inst = match const.proof_entry_universes with
+  | Entries.Monomorphic_entry _ -> EConstr.EInstance.empty
+  | Entries.Polymorphic_entry (_, ctx) ->
+    (* We mimic what the kernel does, that is ensuring that no additional
+       constraints appear in the body of polymorphic constants. Ideally this
+       should be enforced statically. *)
+    let (_, body_uctx), _ = Future.force const.proof_entry_body in
+    let () = assert (Univ.ContextSet.is_empty body_uctx) in
+    EConstr.EInstance.make (Univ.UContext.instance ctx)
+  in
+  let args = List.map EConstr.of_constr args in
+  let lem = EConstr.mkConstU (cst, inst) in
+  let effs = Evd.concat_side_effects eff effs in
+  effs, sigma, lem, args, safe
+
+let get_goal_context pf i =
+  let p = get pf in
+  Proof.get_goal_context_gen p i
+
+let get_current_goal_context pf =
+  let p = get pf in
+  try Proof.get_goal_context_gen p 1
+  with
+  | Proof.NoSuchGoal _ ->
+    (* spiwack: returning empty evar_map, since if there is no goal,
+       under focus, there is no accessible evar either. EJGA: this
+       seems strange, as we have pf *)
+    let env = Global.env () in
+    Evd.from_env env, env
+
+let get_current_context pf =
+  let p = get pf in
+  Proof.get_proof_context p
+
+(* Support for mutually proved theorems *)
+
 (* XXX: this should be unified with the code for non-interactive
    mutuals previously on this file. *)
 module MutualEntry : sig
 
   val declare_variable
-    : info:Info.t
+    : pinfo:Proof_info.t
     -> uctx:UState.t
     -> Entries.parameter_entry
     -> Names.GlobRef.t list
 
   val declare_mutdef
     (* Common to all recthms *)
-    : info:Info.t
+    : pinfo:Proof_info.t
     -> uctx:UState.t
-    -> Evd.side_effects proof_entry
+    -> entry:Evd.side_effects proof_entry
     -> Names.GlobRef.t list
 
 end = struct
@@ -1788,8 +1884,9 @@ end = struct
         Pp.(str "Not a proof by induction: " ++
             Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".")
 
-  let declare_mutdef ~uctx ~info pe i Recthm.{ name; impargs; typ; _} =
-    let { Info.hook; scope; kind; compute_guard; _ } = info in
+  let declare_mutdef ~uctx ~pinfo pe i CInfo.{ name; impargs; typ; _} =
+    let { Proof_info.info; compute_guard; _ } = pinfo in
+    let { Info.hook; scope; kind; _ } = info in
     (* if i = 0 , we don't touch the type; this is for compat
        but not clear it is the right thing to do.
     *)
@@ -1808,25 +1905,25 @@ end = struct
     in
     declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe
 
-  let declare_mutdef ~info ~uctx const =
-    let pe = match info.Info.compute_guard with
+  let declare_mutdef ~pinfo ~uctx ~entry =
+    let pe = match pinfo.Proof_info.compute_guard with
     | [] ->
       (* Not a recursive statement *)
-      const
+      entry
     | possible_indexes ->
       (* Try all combinations... not optimal *)
       let env = Global.env() in
-      Internal.map_entry_body const
+      Internal.map_entry_body entry
         ~f:(guess_decreasing env possible_indexes)
     in
-    List.map_i (declare_mutdef ~info ~uctx pe) 0 info.Info.thms
+    List.map_i (declare_mutdef ~pinfo ~uctx pe) 0 pinfo.Proof_info.cinfo
 
-  let declare_variable ~info ~uctx pe =
-    let { Info.scope; hook } = info in
+  let declare_variable ~pinfo ~uctx pe =
+    let { Info.scope; hook } = pinfo.Proof_info.info in
     List.map_i (
-      fun i { Recthm.name; typ; impargs } ->
+      fun i { CInfo.name; typ; impargs } ->
         declare_assumption ~name ~scope ~hook ~impargs ~uctx pe
-    ) 0 info.Info.thms
+    ) 0 pinfo.Proof_info.cinfo
 
 end
 
@@ -1854,41 +1951,33 @@ let compute_proof_using_for_admitted proof typ pproofs =
       Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
     | _ -> None
 
-let finish_admitted ~info ~uctx pe =
-  let cst = MutualEntry.declare_variable ~info ~uctx pe in
+let finish_admitted ~pinfo ~uctx pe =
+  let cst = MutualEntry.declare_variable ~pinfo ~uctx pe in
   (* If the constant was an obligation we need to update the program map *)
-  match CEphemeron.get info.Info.proof_ending with
+  match CEphemeron.get pinfo.Proof_info.proof_ending with
   | Proof_ending.End_obligation oinfo ->
-    Obls.obligation_admitted_terminator oinfo uctx (List.hd cst)
+    Obls_.obligation_admitted_terminator oinfo uctx (List.hd cst)
   | _ -> ()
 
-let save_lemma_admitted ~proof ~info  =
+let save_admitted ~proof =
   let udecl = get_universe_decl proof in
-  let Proof.{ poly; entry } = Proof.data (get_proof proof) in
+  let Proof.{ poly; entry } = Proof.data (get proof) in
   let typ = match Proofview.initial_goals entry with
     | [typ] -> snd typ
     | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.")
   in
   let typ = EConstr.Unsafe.to_constr typ in
-  let iproof = get_proof proof in
+  let iproof = get proof in
   let pproofs = Proof.partial_proof iproof in
   let sec_vars = compute_proof_using_for_admitted proof typ pproofs in
   let uctx = get_initial_euctx proof in
   let univs = UState.check_univ_decl ~poly uctx udecl in
-  finish_admitted ~info ~uctx (sec_vars, (typ, univs), None)
+  finish_admitted ~pinfo:proof.pinfo ~uctx (sec_vars, (typ, univs), None)
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
 (************************************************************************)
 
-let finish_proved po info =
-  match po with
-  | { entries=[const]; uctx } ->
-    let _r : Names.GlobRef.t list = MutualEntry.declare_mutdef ~info ~uctx const in
-    ()
-  | _ ->
-    CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term")
-
 let finish_derived ~f ~name ~entries =
   (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *)
 
@@ -1921,8 +2010,8 @@ let finish_derived ~f ~name ~entries =
   (* The same is done in the body of the proof. *)
   let lemma_def = Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in
   let lemma_def = DefinitionEntry lemma_def in
-  let _ : Names.Constant.t = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
-  ()
+  let ct = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
+  [GlobRef.ConstRef ct]
 
 let finish_proved_equations ~kind ~hook i proof_obj types sigma0 =
 
@@ -1941,19 +2030,29 @@ let finish_proved_equations ~kind ~hook i proof_obj types sigma0 =
         sigma, cst) sigma0
       types proof_obj.entries
   in
-  hook recobls sigma
+  hook recobls sigma;
+  List.map (fun cst -> GlobRef.ConstRef cst) recobls
+
+let check_single_entry { entries; uctx } label =
+  match entries with
+  | [entry] -> entry, uctx
+  | _ ->
+    CErrors.anomaly ~label Pp.(str "close_proof returned more than one proof term")
 
 let finalize_proof proof_obj proof_info =
   let open Proof_ending in
-  match CEphemeron.default proof_info.Info.proof_ending Regular with
+  match CEphemeron.default proof_info.Proof_info.proof_ending Regular with
   | Regular ->
-    finish_proved proof_obj proof_info
+    let entry, uctx = check_single_entry proof_obj "Proof.save" in
+    MutualEntry.declare_mutdef ~entry ~uctx ~pinfo:proof_info
   | End_obligation oinfo ->
-    Obls.obligation_terminator proof_obj.entries proof_obj.uctx oinfo
+    let entry, uctx = check_single_entry proof_obj "Obligation.save" in
+    Obls_.obligation_terminator ~entry ~uctx ~oinfo
   | End_derive { f ; name } ->
     finish_derived ~f ~name ~entries:proof_obj.entries
   | End_equations { hook; i; types; sigma } ->
-    finish_proved_equations ~kind:proof_info.Info.kind ~hook i proof_obj types sigma
+    let kind = proof_info.Proof_info.info.Info.kind in
+    finish_proved_equations ~kind ~hook i proof_obj types sigma
 
 let err_save_forbidden_in_place_of_qed () =
   CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode")
@@ -1963,24 +2062,24 @@ let process_idopt_for_save ~idopt info =
   | None -> info
   | Some { CAst.v = save_name } ->
     (* Save foo was used; we override the info in the first theorem *)
-    let thms =
-      match info.Info.thms, CEphemeron.default info.Info.proof_ending Proof_ending.Regular with
-      | [ { Recthm.name; _} as decl ], Proof_ending.Regular ->
-        [ { decl with Recthm.name = save_name } ]
+    let cinfo =
+      match info.Proof_info.cinfo, CEphemeron.default info.Proof_info.proof_ending Proof_ending.Regular with
+      | [ { CInfo.name; _} as decl ], Proof_ending.Regular ->
+        [ { decl with CInfo.name = save_name } ]
       | _ ->
         err_save_forbidden_in_place_of_qed ()
-    in { info with Info.thms }
+    in { info with Proof_info.cinfo }
 
-let save_lemma_proved ~proof ~info ~opaque ~idopt =
+let save ~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.pinfo in
   finalize_proof proof_obj proof_info
 
 (***********************************************************************)
 (* Special case to close a lemma without forcing a proof               *)
 (***********************************************************************)
-let save_lemma_admitted_delayed ~proof ~info =
+let save_lemma_admitted_delayed ~proof ~pinfo =
   let { entries; uctx } = proof in
   if List.length entries <> 1 then
     CErrors.user_err Pp.(str "Admitted does not support multiple statements");
@@ -1993,29 +2092,429 @@ let save_lemma_admitted_delayed ~proof ~info =
     | Some typ -> typ in
   let ctx = UState.univ_entry ~poly uctx in
   let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
-  finish_admitted ~uctx ~info (sec_vars, (typ, ctx), None)
+  finish_admitted ~uctx ~pinfo (sec_vars, (typ, ctx), None)
 
-let save_lemma_proved_delayed ~proof ~info ~idopt =
+let save_lemma_proved_delayed ~proof ~pinfo ~idopt =
   (* vio2vo calls this but with invalid info, we have to workaround
      that to add the name to the info structure *)
-  if CList.is_empty info.Info.thms then
+  if CList.is_empty pinfo.Proof_info.cinfo then
     let name = get_po_name proof in
-    let info = Info.add_first_thm ~info ~name ~typ:EConstr.mkSet ~impargs:[] in
+    let info = Proof_info.add_first_thm ~pinfo ~name ~typ:EConstr.mkSet ~impargs:[] in
     finalize_proof proof info
   else
-    let info = process_idopt_for_save ~idopt info in
+    let info = process_idopt_for_save ~idopt pinfo in
     finalize_proof proof info
 
-module Proof = struct
-  type nonrec t = t
-  let get_proof = get_proof
-  let get_proof_name = get_proof_name
-  let map_proof = map_proof
-  let map_fold_proof = map_fold_proof
-  let map_fold_proof_endline = map_fold_proof_endline
-  let set_endline_tactic = set_endline_tactic
-  let set_used_variables = set_used_variables
-  let compact = compact_the_proof
-  let update_global_env = update_global_env
-  let get_open_goals = get_open_goals
+end (* Proof module *)
+
+let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme
+let _ = Abstract.declare_abstract := Proof.declare_abstract
+
+let build_by_tactic = Proof.build_by_tactic
+
+(* This module could be merged with Obl, and placed before [Proof],
+   however there is a single dependency on [Proof.start] for the interactive case *)
+module Obls = struct
+(* For the records fields, opens should go away one these types are private *)
+open Obls_
+open Obls_.Obligation
+open Obls_.ProgramDecl
+
+let reduce c =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota env sigma (EConstr.of_constr c))
+
+let explain_no_obligations = function
+    Some ident -> str "No obligations for program " ++ Id.print ident
+  | None -> str "No obligations remaining"
+
+module Error = struct
+
+  let no_obligations n =
+    CErrors.user_err (explain_no_obligations n)
+
+  let ambiguous_program id ids =
+    CErrors.user_err
+      Pp.(str "More than one program with unsolved obligations: " ++ prlist Id.print ids
+          ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print id ++ str "\"")
+
+  let unknown_obligation num =
+    CErrors.user_err (Pp.str (Printf.sprintf "Unknown obligation number %i" (succ num)))
+
+  let already_solved num =
+    CErrors.user_err
+      ( str "Obligation" ++ spc () ++ int num ++ str "already" ++ spc ()
+        ++ str "solved." )
+
+  let depends num rem =
+    CErrors.user_err
+      ( str "Obligation " ++ int num
+        ++ str " depends on obligation(s) "
+        ++ pr_sequence (fun x -> int (succ x)) rem)
+
+end
+
+let default_tactic = ref (Proofview.tclUNIT ())
+
+let evar_of_obligation o = Evd.make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
+
+let subst_deps expand obls deps t =
+  let osubst = Obls_.obl_substitution expand obls deps in
+    (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
+
+let subst_deps_obl obls obl =
+  let t' = subst_deps true obls obl.obl_deps obl.obl_type in
+  Obligation.set_type ~typ:t' obl
+
+open Evd
+
+let is_defined obls x = not (Option.is_empty obls.(x).obl_body)
+
+let deps_remaining obls deps =
+  Int.Set.fold
+    (fun x acc ->
+      if is_defined obls x then acc
+      else x :: acc)
+    deps []
+
+let goal_kind = Decls.(IsDefinition Definition)
+let goal_proof_kind = Decls.(IsProof Lemma)
+
+let kind_of_obligation o =
+  match o with
+  | Evar_kinds.Define false
+  | Evar_kinds.Expand -> goal_kind
+  | _ -> goal_proof_kind
+
+(* Solve an obligation using tactics, return the corresponding proof term *)
+let warn_solve_errored =
+  CWarnings.create ~name:"solve_obligation_error" ~category:"tactics"
+    (fun err ->
+      Pp.seq
+        [ str "Solve Obligations tactic returned error: "
+        ; err
+        ; fnl ()
+        ; str "This will become an error in the future" ])
+
+let solve_by_tac ?loc name evi t ~poly ~uctx =
+  (* the status is dropped. *)
+  try
+    let env = Global.env () in
+    let body, types, _univs, _, uctx =
+      build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in
+    Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body);
+    Some (body, types, uctx)
+  with
+  | Refiner.FailError (_, s) as exn ->
+    let _ = Exninfo.capture exn in
+    CErrors.user_err ?loc ~hdr:"solve_obligation" (Lazy.force s)
+  (* If the proof is open we absorb the error and leave the obligation open *)
+  | Proof_.OpenProof _ ->
+    None
+  | e when CErrors.noncritical e ->
+    let err = CErrors.print e in
+    warn_solve_errored ?loc err;
+    None
+
+let get_unique_prog prg =
+  match State.get_unique_open_prog prg with
+  | Ok prg -> prg
+  | Error [] ->
+    Error.no_obligations None
+  | Error ((id :: _) as ids) ->
+    Error.ambiguous_program id ids
+
+let rec solve_obligation prg num tac =
+  let user_num = succ num in
+  let { obls; remaining=rem } = Internal.get_obligations prg in
+  let obl = obls.(num) in
+  let remaining = deps_remaining obls obl.obl_deps in
+  let () =
+    if not (Option.is_empty obl.obl_body)
+    then Error.already_solved user_num;
+    if not (List.is_empty remaining)
+    then Error.depends user_num remaining
+  in
+  let obl = subst_deps_obl obls obl in
+  let scope = Locality.Global Locality.ImportNeedQualified in
+  let kind = kind_of_obligation (snd obl.obl_status) in
+  let evd = Evd.from_ctx (Internal.get_uctx prg) in
+  let evd = Evd.update_sigma_env evd (Global.env ()) in
+  let auto n oblset tac = auto_solve_obligations n ~oblset tac in
+  let proof_ending =
+    let name = Internal.get_name prg in
+    Proof_ending.End_obligation {name; num; auto}
+  in
+  let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) () in
+  let poly = Internal.get_poly prg in
+  let info = Info.make ~scope ~kind ~poly () in
+  let lemma = Proof.start_core ~cinfo ~info ~proof_ending evd  in
+  let lemma = fst @@ Proof.by !default_tactic lemma in
+  let lemma = Option.cata (fun tac -> Proof.set_endline_tactic tac lemma) lemma tac in
+  lemma
+
+and obligation (user_num, name, typ) tac =
+  let num = pred user_num in
+  let prg = get_unique_prog name in
+  let { obls; remaining } = Internal.get_obligations prg in
+  if num >= 0 && num < Array.length obls then
+    let obl = obls.(num) in
+    match obl.obl_body with
+    | None -> solve_obligation prg num tac
+    | Some r -> Error.already_solved num
+  else Error.unknown_obligation num
+
+and solve_obligation_by_tac prg obls i tac =
+  let obl = obls.(i) in
+    match obl.obl_body with
+    | Some _ -> None
+    | None ->
+      if List.is_empty (deps_remaining obls obl.obl_deps) then
+        let obl = subst_deps_obl obls obl in
+        let tac =
+          match tac with
+          | Some t -> t
+          | None ->
+            match obl.obl_tac with
+            | Some t -> t
+            | None -> !default_tactic
+        in
+        let uctx = Internal.get_uctx prg in
+        let uctx = UState.update_sigma_env uctx (Global.env ()) in
+        let poly = Internal.get_poly prg in
+        match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac ~poly ~uctx with
+        | None -> None
+        | Some (t, ty, uctx) ->
+          let prg = ProgramDecl.Internal.set_uctx ~uctx prg in
+          let def, obl', _cst = declare_obligation prg obl ~body:t ~types:ty ~uctx in
+          obls.(i) <- obl';
+          if def && not poly then (
+            (* Declare the term constraints with the first obligation only *)
+            let uctx_global = UState.from_env (Global.env ()) in
+            let uctx = UState.merge_subst uctx_global (UState.subst uctx) in
+            Some (ProgramDecl.Internal.set_uctx ~uctx prg))
+          else Some prg
+      else None
+
+and solve_prg_obligations prg ?oblset tac =
+  let { obls; remaining } = Internal.get_obligations prg in
+  let rem = ref remaining in
+  let obls' = Array.copy obls in
+  let set = ref Int.Set.empty in
+  let p = match oblset with
+    | None -> (fun _ -> true)
+    | Some s -> set := s;
+      (fun i -> Int.Set.mem i !set)
+  in
+  let (), prg =
+    Array.fold_left_i
+      (fun i ((), prg) x ->
+        if p i then (
+          match solve_obligation_by_tac prg obls' i tac with
+          | None -> (), prg
+          | Some prg ->
+            let deps = dependencies obls i in
+            set := Int.Set.union !set deps;
+            decr rem;
+            (), prg)
+        else (), prg)
+      ((), prg) obls'
+  in
+  update_obls prg obls' !rem
+
+and solve_obligations n tac =
+  let prg = get_unique_prog n in
+    solve_prg_obligations prg tac
+
+and solve_all_obligations tac =
+  State.fold ~init:() ~f:(fun k v () ->
+      let _ = solve_prg_obligations v tac in ())
+
+and try_solve_obligation n prg tac =
+  let prg = get_unique_prog prg in
+  let {obls; remaining} = Internal.get_obligations prg in
+  let obls' = Array.copy obls in
+  match solve_obligation_by_tac prg obls' n tac with
+  | Some prg' ->
+    let _r = update_obls prg' obls' (pred remaining) in
+    ()
+  | None -> ()
+
+and try_solve_obligations n tac =
+  let _ = solve_obligations n tac in
+  ()
+
+and auto_solve_obligations n ?oblset tac : progress =
+  Flags.if_verbose Feedback.msg_info
+    (str "Solving obligations automatically...");
+  let prg = get_unique_prog n in
+  solve_prg_obligations prg ?oblset tac
+
+let show_single_obligation i n obls x =
+  let x = subst_deps_obl obls x in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let msg =
+    str "Obligation" ++ spc ()
+    ++ int (succ i)
+    ++ spc () ++ str "of" ++ spc () ++ Id.print n ++ str ":" ++ spc ()
+    ++ hov 1 (Printer.pr_constr_env env sigma x.obl_type
+              ++ str "." ++ fnl ()) in
+  Feedback.msg_info msg
+
+let show_obligations_of_prg ?(msg = true) prg =
+  let n = Internal.get_name prg in
+  let {obls; remaining} = Internal.get_obligations prg in
+  let showed = ref 5 in
+    if msg then Feedback.msg_info (int remaining ++ str " obligation(s) remaining: ");
+    Array.iteri
+      (fun i x ->
+         match x.obl_body with
+         | None ->
+           if !showed > 0 then begin
+             decr showed;
+             show_single_obligation i n obls x
+           end
+         | Some _ -> ())
+      obls
+
+let show_obligations ?(msg = true) n =
+  let progs =
+    match n with
+    | None ->
+      State.all ()
+    | Some n ->
+      (match State.find n with
+       | Some prg -> [prg]
+       | None -> Error.no_obligations (Some n))
+  in
+  List.iter (fun x -> show_obligations_of_prg ~msg x) progs
+
+let show_term n =
+  let prg = get_unique_prog n in
+  ProgramDecl.show prg
+
+let msg_generating_obl name obls =
+  let len = Array.length obls in
+  let info = Id.print name ++ str " has type-checked" in
+  Feedback.msg_info
+    (if len = 0 then info ++ str "."
+     else
+       info ++ str ", generating " ++ int len ++
+       str (String.plural len " obligation"))
+
+let add_definition ~cinfo ~info ?term ~uctx
+    ?tactic ?(reduce = reduce) ?(opaque = false) obls =
+  let prg =
+    ProgramDecl.make ~info ~cinfo ~body:term ~opaque ~uctx ~reduce ~ntns:[] ~deps:[] ~fixpoint_kind:None obls
+  in
+  let name = CInfo.get_name cinfo in
+  let {obls;_} = Internal.get_obligations prg in
+  if Int.equal (Array.length obls) 0 then (
+    Flags.if_verbose (msg_generating_obl name) obls;
+    let cst = Obls_.declare_definition prg in
+    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 ->
+      Flags.if_verbose (show_obligations ~msg:false) (Some name);
+      res
+    | _ -> res
+
+let add_mutual_definitions l ~info ~uctx
+    ?tactic ?(reduce = reduce) ?(opaque = false) ~ntns fixkind =
+  let deps = List.map (fun (ci,_,_) -> CInfo.get_name ci) l in
+  let pm =
+    List.fold_left
+      (fun () (cinfo, b, obls) ->
+        let prg =
+          ProgramDecl.make ~info ~cinfo ~opaque ~body:(Some b) ~uctx ~deps
+            ~fixpoint_kind:(Some fixkind) ~ntns obls ~reduce
+        in
+        State.add (CInfo.get_name cinfo) prg)
+      () l
+  in
+  let pm, _defined =
+    List.fold_left
+      (fun (pm, finished) x ->
+        if finished then (pm, finished)
+        else
+          let res = auto_solve_obligations (Some x) tactic in
+          match res with
+          | Defined _ ->
+            (* If one definition is turned into a constant,
+               the whole block is defined. *)
+            (pm, true)
+          | _ -> (pm, false))
+      (pm, false) deps
+  in
+  pm
+
+let admit_prog prg =
+  let {obls; remaining} = Internal.get_obligations prg in
+  let obls = Array.copy obls in
+    Array.iteri
+      (fun i x ->
+        match x.obl_body with
+        | None ->
+            let x = subst_deps_obl obls x in
+            let uctx = Internal.get_uctx prg in
+            let univs = UState.univ_entry ~poly:false uctx in
+            let kn = declare_constant ~name:x.obl_name ~local:Locality.ImportNeedQualified
+              (ParameterEntry (None, (x.obl_type, univs), None)) ~kind:Decls.(IsAssumption Conjectural)
+            in
+              assumption_message x.obl_name;
+              obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x
+        | Some _ -> ())
+      obls;
+  Obls_.update_obls prg obls 0
+
+(* get_any_prog *)
+let rec admit_all_obligations () =
+  let prg = State.first_pending () in
+  match prg with
+  | None -> ()
+  | Some prg ->
+    let _prog = admit_prog prg in
+    admit_all_obligations ()
+
+let admit_obligations n =
+  match n with
+  | None -> admit_all_obligations ()
+  | Some _ ->
+    let prg = get_unique_prog n in
+    let _ = admit_prog prg in
+    ()
+
+let next_obligation n tac =
+  let prg = match n with
+    | None -> State.first_pending () |> Option.get
+    | Some _ -> get_unique_prog n
+  in
+  let {obls; remaining} = Internal.get_obligations prg in
+  let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
+  let i = match Array.findi is_open obls with
+    | Some i -> i
+    | None -> CErrors.anomaly (Pp.str "Could not find a solvable obligation.")
+  in
+  solve_obligation prg i tac
+
+let check_program_libraries () =
+  Coqlib.check_required_library Coqlib.datatypes_module_name;
+  Coqlib.check_required_library ["Coq";"Init";"Specif"];
+  Coqlib.check_required_library ["Coq";"Program";"Tactics"]
+
+(* aliases *)
+module State = Obls_.State
+let prepare_obligation = prepare_obligation
+let check_solved_obligations = Obls_.check_solved_obligations
+type fixpoint_kind = Obls_.fixpoint_kind =
+  | IsFixpoint of lident option list | IsCoFixpoint
+type nonrec progress = progress =
+  | Remain of int | Dependent | Defined of GlobRef.t
+
 end
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 979bdd4334..4891e66803 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -9,25 +9,23 @@
 (************************************************************************)
 
 open Names
-open Constr
-open Entries
 
-(** This module provides the official functions to declare new
+(** This module provides the functions to declare new
    variables, parameters, constants and inductive types in the global
    environment. It also updates some accesory tables such as [Nametab]
    (name resolution), [Impargs], and [Notations]. *)
 
-(** We provide two kind of functions:
+(** We provide three main entry points:
 
   - one-go functions, that will register a constant in one go, suited
    for non-interactive definitions where the term is given.
 
-  - two-phase [start/declare] functions which will create an
-   interactive proof, allow its modification, and saving when
-   complete.
+  - two-phase [start/save] functions which will create an
+   interactive proof, allow its modification using tactics, and saving
+   when complete.
 
-  Internally, these functions mainly differ in that usually, the first
-  case doesn't require setting up the tactic engine.
+  - program mode API, that allow to declare a constant with holes, to
+   be fullfilled later.
 
   Note that the API in this file is still in a state of flux, don't
   hesitate to contact the maintainers if you have any question.
@@ -38,27 +36,196 @@ open Entries
 
  *)
 
+(** Declaration hooks, to be run when a constant is saved. Use with
+   care, as imperative effects may become not supported in the
+   future. *)
+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
+
+(** {2 One-go, non-interactive declaration API } *)
+
+(** Information for a single top-level named constant *)
+module CInfo : sig
+  type 'constr t
+
+  val make :
+    name : Id.t
+    -> typ:'constr
+    -> ?args:Name.t list
+    -> ?impargs:Impargs.manual_implicits
+    -> unit
+    -> 'constr t
+
+  (* Used only in Vernacentries, may disappear from public API *)
+  val to_constr : Evd.evar_map -> EConstr.t t -> Constr.t t
+
+  (* Used only in RecLemmas, may disappear from public API *)
+  val get_typ : 'constr t -> 'constr
+
+end
+
+(** Information for a declaration, interactive or not, includes
+   parameters shared by mutual constants *)
+module Info : sig
+
+  type t
+
+  (** Note that [opaque] doesn't appear here as it is not known at the
+     start of the proof in the interactive case. *)
+  val make
+    : ?poly:bool
+    -> ?inline : bool
+    -> ?kind : Decls.logical_kind
+    (** Theorem, etc... *)
+    -> ?udecl : UState.universe_decl
+    -> ?scope : Locality.locality
+    (** locality  *)
+    -> ?hook : Hook.t
+    (** Callback to be executed after saving the constant *)
+    -> unit
+    -> t
+
+end
+
+(** Declares a non-interactive constant; [body] and [types] will be
+   normalized w.r.t. the passed [evar_map] [sigma]. Universes should
+   be handled properly, including minimization and restriction. Note
+   that [sigma] is checked for unresolved evars, thus you should be
+   careful not to submit open terms or evar maps with stale,
+   unresolved existentials *)
+val declare_definition
+  :  info:Info.t
+  -> cinfo:EConstr.t option CInfo.t
+  -> opaque:bool
+  -> body:EConstr.t
+  -> Evd.evar_map
+  -> GlobRef.t
+
+val declare_assumption
+  :  name:Id.t
+  -> scope:Locality.locality
+  -> hook:Hook.t option
+  -> impargs:Impargs.manual_implicits
+  -> uctx:UState.t
+  -> Entries.parameter_entry
+  -> GlobRef.t
+
+type lemma_possible_guards = int list list
+
+val declare_mutually_recursive
+  : info:Info.t
+  -> cinfo: Constr.t CInfo.t list
+  -> opaque:bool
+  -> ntns:Vernacexpr.decl_notation list
+  -> uctx:UState.t
+  -> rec_declaration:Constr.rec_declaration
+  -> possible_indexes:lemma_possible_guards option
+  -> Names.GlobRef.t list
+
+(** {2 Declaration of interactive constants }  *)
+
 (** [Declare.Proof.t] Construction of constants using interactive proofs. *)
 module Proof : sig
 
   type t
 
-  (** 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
+  (** [start_proof ~info ~cinfo sigma] starts a proof of [cinfo].
+      The proof is started in the evar map [sigma] (which
+      can typically contain universe constraints) *)
+  val start
+    :  info:Info.t
+    -> cinfo:EConstr.t CInfo.t
+    -> Evd.evar_map
+    -> t
+
+  (** [start_{derive,equations}] are functions meant to handle
+     interactive proofs with multiple goals, they should be considered
+     experimental until we provide a more general API encompassing
+     both of them. Please, get in touch with the developers if you
+     would like to experiment with multi-goal dependent proofs so we
+     can use your input on the design of the new API. *)
+  val start_derive : f:Id.t -> name:Id.t -> info:Info.t -> Proofview.telescope -> t
+
+  val start_equations :
+       name:Id.t
+    -> info:Info.t
+    -> hook:(Constant.t list -> Evd.evar_map -> unit)
+    -> types:(Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
+    -> Evd.evar_map
+    -> Proofview.telescope
+    -> t
+
+  (** Pretty much internal, used by the Lemma vernaculars *)
+  val start_with_initialization
+    :  info:Info.t
+    -> cinfo:Constr.t CInfo.t
+    -> Evd.evar_map
+    -> t
+
+  type mutual_info = (bool * lemma_possible_guards * Constr.t option list option)
+
+  (** Pretty much internal, used by mutual Lemma / Fixpoint vernaculars *)
+  val start_mutual_with_initialization
+    :  info:Info.t
+    -> cinfo:Constr.t CInfo.t list
+    -> mutual_info:mutual_info
+    -> Evd.evar_map
+    -> int list option
+    -> t
+
+  (** Qed a proof  *)
+  val save
+    : proof:t
+    -> opaque:Vernacexpr.opacity_flag
+    -> idopt:Names.lident option
+    -> GlobRef.t list
+
+  (** Admit a proof *)
+  val save_admitted : proof:t -> unit
 
-  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
+  (** [by tac] applies tactic [tac] to the 1st subgoal of the current
+      focused proof.
+      Returns [false] if an unsafe tactic has been used. *)
+  val by : unit Proofview.tactic -> t -> t * bool
+
+  (** Operations on ongoing proofs *)
+  val get : t -> Proof.t
+  val get_name : t -> Names.Id.t
+
+  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
 
   (** Sets the section variables assumed by the proof, returns its closure
    * (w.r.t. type dependencies and let-ins covered by it) *)
-  val set_used_variables : t ->
-    Names.Id.t list -> Constr.named_context * t
+  val set_used_variables : t -> Names.Id.t list -> Constr.named_context * t
 
   val compact : t -> t
 
@@ -69,32 +236,73 @@ module Proof : sig
 
   val get_open_goals : t -> int
 
-end
+  (** Helpers to obtain proof state when in an interactive proof *)
 
-type opacity_flag = Vernacexpr.opacity_flag = Opaque | Transparent
+  (** [get_goal_context n] returns the context of the [n]th subgoal of
+      the current focused proof or raises a [UserError] if there is no
+      focused proof or if there is no more subgoals *)
 
-(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
-   name [name] with goals [goals] (a list of pairs of environment and
-   conclusion); [poly] determines if the proof is universe
-   polymorphic. The proof is started in the evar map [sigma] (which
-   can typically contain universe constraints), and with universe
-   bindings [udecl]. *)
-val start_proof
-  :  name:Names.Id.t
-  -> udecl:UState.universe_decl
-  -> poly:bool
-  -> Evd.evar_map
-  -> (Environ.env * EConstr.types) list
-  -> Proof.t
+  val get_goal_context : t -> int -> Evd.evar_map * Environ.env
 
-(** Like [start_proof] except that there may be dependencies between
-    initial goals. *)
-val start_dependent_proof
-  :  name:Names.Id.t
-  -> udecl:UState.universe_decl
-  -> poly:bool
-  -> Proofview.telescope
-  -> Proof.t
+  (** [get_current_goal_context ()] works as [get_goal_context 1] *)
+  val get_current_goal_context : t -> Evd.evar_map * Environ.env
+
+  (** [get_current_context ()] returns the context of the
+      current focused goal. If there is no focused goal but there
+      is a proof in progress, it returns the corresponding evar_map.
+      If there is no pending proof then it returns the current global
+      environment and empty evar_map. *)
+  val get_current_context : t -> Evd.evar_map * Environ.env
+
+  (* Internal, don't use *)
+  module Proof_info : sig
+    type t
+    (* Make a dummy value, used in the stm *)
+    val default : unit -> t
+  end
+  val info : t -> Proof_info.t
+
+  (** {2 Proof delay API, warning, internal, not stable *)
+
+  (* Intermediate step necessary to delegate the future.
+   * Both access the current proof state. The former is supposed to be
+   * chained with a computation that completed the proof *)
+  type closed_proof_output
+
+  (** Requires a complete proof. *)
+  val return_proof : t -> closed_proof_output
+
+  (** An incomplete proof is allowed (no error), and a warn is given if
+      the proof is complete. *)
+  val return_partial_proof : t -> closed_proof_output
+
+  (** XXX: This is an internal, low-level API and could become scheduled
+      for removal from the public API, use higher-level declare APIs
+      instead *)
+  type proof_object
+
+  val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> t -> proof_object
+  val close_future_proof : feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> proof_object
+
+  (** Special cases for delayed proofs, in this case we must provide the
+      proof information so the proof won't be forced. *)
+  val save_lemma_admitted_delayed :
+    proof:proof_object
+    -> pinfo:Proof_info.t
+    -> unit
+
+  val save_lemma_proved_delayed
+    : proof:proof_object
+    -> pinfo:Proof_info.t
+    -> idopt:Names.lident option
+    -> GlobRef.t list
+
+  (** Used by the STM only to store info, should go away *)
+  val get_po_name : proof_object -> Id.t
+
+end
+
+(** {2 low-level, internla API, avoid using unless you have special needs } *)
 
 (** Proof entries represent a proof that has been finished, but still
    not registered with the kernel.
@@ -104,30 +312,32 @@ val start_dependent_proof
    instead *)
 type 'a proof_entry
 
-(** XXX: This is an internal, low-level API and could become scheduled
-   for removal from the public API, use higher-level declare APIs
-   instead *)
-type proof_object
-
-(** Used by the STM only to store info, should go away *)
-val get_po_name : proof_object -> Id.t
-
-val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t -> proof_object
-
-(** Declaration of local constructions (Variable/Hypothesis/Local) *)
+val definition_entry
+  :  ?opaque:bool
+  -> ?inline:bool
+  -> ?types:Constr.types
+  -> ?univs:Entries.universes_entry
+  -> Constr.constr
+  -> Evd.side_effects proof_entry
 
 (** XXX: This is an internal, low-level API and could become scheduled
-   for removal from the public API, use higher-level declare APIs
-   instead *)
-type 'a constant_entry =
-  | DefinitionEntry of 'a proof_entry
-  | ParameterEntry of parameter_entry
-  | PrimitiveEntry of primitive_entry
+    for removal from the public API, use higher-level declare APIs
+    instead *)
+val declare_entry
+  :  name:Id.t
+  -> scope:Locality.locality
+  -> kind:Decls.logical_kind
+  -> ?hook:Hook.t
+  -> impargs:Impargs.manual_implicits
+  -> uctx:UState.t
+  -> Evd.side_effects proof_entry
+  -> GlobRef.t
 
+(** Declaration of local constructions (Variable/Hypothesis/Local) *)
 val declare_variable
   :  name:variable
   -> kind:Decls.logical_kind
-  -> typ:types
+  -> typ:Constr.types
   -> impl:Glob_term.binding_kind
   -> unit
 
@@ -137,34 +347,33 @@ val declare_variable
    XXX: This is an internal, low-level API and could become scheduled
    for removal from the public API, use higher-level declare APIs
    instead *)
-val definition_entry
-  :  ?opaque:bool
-  -> ?inline:bool
-  -> ?types:types
-  -> ?univs:Entries.universes_entry
-  -> constr
-  -> Evd.side_effects proof_entry
+type 'a constant_entry =
+  | DefinitionEntry of 'a proof_entry
+  | ParameterEntry of Entries.parameter_entry
+  | PrimitiveEntry of Entries.primitive_entry
 
-type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeedQualified
+val prepare_parameter
+  : poly:bool
+  -> udecl:UState.universe_decl
+  -> types:EConstr.types
+  -> Evd.evar_map
+  -> Evd.evar_map * Entries.parameter_entry
 
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
    the full path of the declaration
 
-  internal specify if the constant has been created by the kernel or by the
-  user, and in the former case, if its errors should be silent
-
   XXX: This is an internal, low-level API and could become scheduled
   for removal from the public API, use higher-level declare APIs
   instead *)
 val declare_constant
-  :  ?local:import_status
+  :  ?local:Locality.import_status
   -> name:Id.t
   -> kind:Decls.logical_kind
   -> Evd.side_effects constant_entry
   -> Constant.t
 
-(** Declaration messages *)
+(** Declaration messages, for internal use *)
 
 (** XXX: Scheduled for removal from public API, do not use *)
 val definition_message : Id.t -> unit
@@ -173,35 +382,6 @@ val fixpoint_message : int array option -> Id.t list -> unit
 
 val check_exists : Id.t -> unit
 
-(** {6 For legacy support, do not use}  *)
-
-module Internal : sig
-
-  type constant_obj
-
-  val objConstant : constant_obj Libobject.Dyn.tag
-  val objVariable : unit Libobject.Dyn.tag
-
-end
-
-(* Intermediate step necessary to delegate the future.
- * Both access the current proof state. The former is supposed to be
- * chained with a computation that completed the proof *)
-type closed_proof_output
-
-(** Requires a complete proof. *)
-val return_proof : Proof.t -> closed_proof_output
-
-(** An incomplete proof is allowed (no error), and a warn is given if
-   the proof is complete. *)
-val return_partial_proof : Proof.t -> closed_proof_output
-val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output Future.computation -> proof_object
-
-(** [by tac] applies tactic [tac] to the 1st subgoal of the current
-    focused proof.
-    Returns [false] if an unsafe tactic has been used. *)
-val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool
-
 (** Semantics of this function is a bit dubious, use with care *)
 val build_by_tactic
   :  ?side_eff:bool
@@ -212,138 +392,77 @@ val build_by_tactic
   -> unit Proofview.tactic
   -> Constr.constr * Constr.types option * Entries.universes_entry * bool * UState.t
 
-(** {6 Helpers to obtain proof state when in an interactive proof } *)
-
-(** [get_goal_context n] returns the context of the [n]th subgoal of
-   the current focused proof or raises a [UserError] if there is no
-   focused proof or if there is no more subgoals *)
-
-val get_goal_context : Proof.t -> int -> Evd.evar_map * Environ.env
+(** {2 Program mode API} *)
+
+(** Coq's Program mode support. This mode extends declarations of
+   constants and fixpoints with [Program Definition] and [Program
+   Fixpoint] to support incremental construction of terms using
+   delayed proofs, called "obligations"
+
+    The mode also provides facilities for managing and auto-solving
+   sets of obligations.
+
+    The basic code flow of programs/obligations is as follows:
+
+    - [add_definition] / [add_mutual_definitions] are called from the
+   respective [Program] vernacular command interpretation; at this
+   point the only extra work we do is to prepare the new definition
+   [d] using [RetrieveObl], which consists in turning unsolved evars
+   into obligations. [d] is not sent to the kernel yet, as it is not
+   complete and cannot be typchecked, but saved in a special
+   data-structure. Auto-solving of obligations is tried at this stage
+   (see below)
+
+   - [next_obligation] will retrieve the next obligation
+   ([RetrieveObl] sorts them by topological order) and will try to
+   solve it. When all obligations are solved, the original constant
+   [d] is grounded and sent to the kernel for addition to the global
+   environment. Auto-solving of obligations is also triggered on
+   obligation completion.
+
+{2} Solving of obligations: Solved obligations are stored as regular
+   global declarations in the global environment, usually with name
+   [constant_obligation_number] where [constant] is the original
+   [constant] and [number] is the corresponding (internal) number.
+
+   Solving an obligation can trigger a bit of a complex cascaded
+   callback path; closing an obligation can indeed allow all other
+   obligations to be closed, which in turn may trigged the declaration
+   of the original constant. Care must be taken, as this can modify
+   [Global.env] in arbitrarily ways. Current code takes some care to
+   refresh the [env] in the proper boundaries, but the invariants
+   remain delicate.
+
+{2} Saving of obligations: as open obligations use the regular proof
+   mode, a `Qed` will call `Lemmas.save_lemma` first. For this reason
+   obligations code is split in two: this file, [Obligations], taking
+   care of the top-level vernac commands, and [Declare], which is
+   called by `Lemmas` to close an obligation proof and eventually to
+   declare the top-level [Program]ed constant.
 
-(** [get_current_goal_context ()] works as [get_goal_context 1] *)
-val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env
-
-(** [get_current_context ()] returns the context of the
-  current focused goal. If there is no focused goal but there
-  is a proof in progress, it returns the corresponding evar_map.
-  If there is no pending proof then it returns the current global
-  environment and empty evar_map. *)
-val get_current_context : Proof.t -> Evd.evar_map * Environ.env
-
-(** XXX: Temporarily re-exported for 3rd party code; don't use  *)
-val build_constant_by_tactic :
-  name:Names.Id.t ->
-  ?opaque:opacity_flag ->
-  uctx:UState.t ->
-  sign:Environ.named_context_val ->
-  poly:bool ->
-  EConstr.types ->
-  unit Proofview.tactic ->
-  Evd.side_effects proof_entry * bool * UState.t
-[@@ocaml.deprecated "This function is deprecated, used newer API in declare"]
+ *)
 
-val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
-[@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"]
+module Obls : sig
 
-type locality = Locality.locality = Discharge | Global of import_status
+type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint
 
-(** Declaration hooks *)
-module Hook : sig
+module State : sig
+  (* Internal *)
   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
+  val prg_tag : t Summary.Dyn.tag
 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 *)
-val declare_entry
-  :  name:Id.t
-  -> scope:locality
-  -> kind:Decls.logical_kind
-  -> ?hook:Hook.t
-  -> impargs:Impargs.manual_implicits
-  -> uctx:UState.t
-  -> Evd.side_effects proof_entry
-  -> GlobRef.t
-
-(** Declares a non-interactive constant; [body] and [types] will be
-   normalized w.r.t. the passed [evar_map] [sigma]. Universes should
-   be handled properly, including minimization and restriction. Note
-   that [sigma] is checked for unresolved evars, thus you should be
-   careful not to submit open terms or evar maps with stale,
-   unresolved existentials *)
-val declare_definition
-  :  name:Id.t
-  -> scope:locality
-  -> kind:Decls.logical_kind
-  -> opaque:bool
-  -> impargs:Impargs.manual_implicits
-  -> udecl:UState.universe_decl
-  -> ?hook:Hook.t
-  -> poly:bool
-  -> ?inline:bool
-  -> types:EConstr.t option
-  -> body:EConstr.t
-  -> Evd.evar_map
-  -> GlobRef.t
-
-val declare_assumption
-  :  name:Id.t
-  -> scope:locality
-  -> hook:Hook.t option
-  -> impargs:Impargs.manual_implicits
-  -> uctx:UState.t
-  -> 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
+(** Check obligations are properly solved before closing the
+   [what_for] section / module *)
+val check_solved_obligations : what_for:Pp.t -> unit
 
-type lemma_possible_guards = int list list
+val default_tactic : unit Proofview.tactic ref
 
-val declare_mutually_recursive
-  : opaque:bool
-  -> scope:locality
-  -> kind:Decls.logical_kind
-  -> poly:bool
-  -> uctx:UState.t
-  -> udecl:UState.universe_decl
-  -> ntns:Vernacexpr.decl_notation list
-  -> rec_declaration:Constr.rec_declaration
-  -> possible_indexes:lemma_possible_guards option
-  -> Recthm.t list
-  -> Names.GlobRef.t list
+(** 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 *)
 
 (** Prepare API, to be removed once we provide the corresponding 1-step API *)
 val prepare_obligation
@@ -353,212 +472,75 @@ val prepare_obligation
   -> Evd.evar_map
   -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info
 
-val prepare_parameter
-  : poly:bool
-  -> udecl:UState.universe_decl
-  -> types:EConstr.types
-  -> Evd.evar_map
-  -> Evd.evar_map * Entries.parameter_entry
-
-(* Compat: will remove *)
-exception AlreadyDeclared of (string option * Names.Id.t)
-
-module Obls : sig
-
-type 'a obligation_body = DefinedObl of 'a | TermObl of constr
-
-module Obligation : sig
-  type t = private
-    { obl_name : Id.t
-    ; obl_type : types
-    ; obl_location : Evar_kinds.t Loc.located
-    ; obl_body : pconstant obligation_body option
-    ; obl_status : bool * Evar_kinds.obligation_definition_status
-    ; obl_deps : Int.Set.t
-    ; obl_tac : unit Proofview.tactic option }
-
-  val set_type : typ:Constr.types -> t -> t
-  val set_body : body:pconstant obligation_body -> t -> t
-end
-
-type obligations = {obls : Obligation.t array; remaining : int}
-type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint
-
-(* Information about a single [Program {Definition,Lemma,..}] declaration *)
-module ProgramDecl : sig
-  type t = private
-    { prg_name : Id.t
-    ; prg_body : constr
-    ; prg_type : constr
-    ; prg_ctx : UState.t
-    ; prg_univdecl : UState.universe_decl
-    ; prg_obligations : obligations
-    ; prg_deps : Id.t list
-    ; prg_fixkind : fixpoint_kind option
-    ; prg_implicits : Impargs.manual_implicits
-    ; prg_notations : Vernacexpr.decl_notation list
-    ; prg_poly : bool
-    ; prg_scope : locality
-    ; prg_kind : Decls.definition_object_kind
-    ; prg_reduce : constr -> constr
-    ; prg_hook : Hook.t option
-    ; prg_opaque : bool }
-
-  val make :
-       ?opaque:bool
-    -> ?hook:Hook.t
-    -> Names.Id.t
-    -> udecl:UState.universe_decl
-    -> uctx:UState.t
-    -> impargs:Impargs.manual_implicits
-    -> poly:bool
-    -> scope:locality
-    -> kind:Decls.definition_object_kind
-    -> Constr.constr option
-    -> Constr.types
-    -> Names.Id.t list
-    -> fixpoint_kind option
-    -> Vernacexpr.decl_notation list
-    -> RetrieveObl.obligation_info
-    -> (Constr.constr -> Constr.constr)
-    -> t
-
-  val set_uctx : uctx:UState.t -> t -> t
-end
-
-(** [declare_obligation prg obl ~uctx ~types ~body] Save an obligation
-   [obl] for program definition [prg] *)
-val declare_obligation :
-     ProgramDecl.t
-  -> Obligation.t
+(** Start a [Program Definition c] proof. [uctx] [udecl] [impargs]
+   [kind] [scope] [poly] etc... come from the interpretation of the
+   vernacular; `obligation_info` was generated by [RetrieveObl] It
+   will return whether all the obligations were solved; if so, it will
+   also register [c] with the kernel. *)
+val add_definition :
+     cinfo:Constr.types CInfo.t
+  -> info:Info.t
+  -> ?term:Constr.t
   -> uctx:UState.t
-  -> types:Constr.types option
-  -> body:Constr.types
-  -> bool * Obligation.t
-
-module State : sig
-
-  val num_pending : unit -> int
-  val first_pending : unit -> ProgramDecl.t option
-
-  (** Returns [Error duplicate_list] if not a single program is open *)
-  val get_unique_open_prog :
-    Id.t option -> (ProgramDecl.t, Id.t list) result
-
-  (** Add a new obligation *)
-  val add : Id.t -> ProgramDecl.t -> unit
-
-  val fold : f:(Id.t -> ProgramDecl.t -> 'a -> 'a) -> init:'a -> 'a
-
-  val all : unit -> ProgramDecl.t list
+  -> ?tactic:unit Proofview.tactic
+  -> ?reduce:(Constr.t -> Constr.t)
+  -> ?opaque:bool
+  -> RetrieveObl.obligation_info
+  -> progress
 
-  val find : Id.t -> ProgramDecl.t option
+(* XXX: unify with MutualEntry *)
 
-  (* Internal *)
-  type t
-  val prg_tag : t Summary.Dyn.tag
-end
-
-val declare_definition : ProgramDecl.t -> Names.GlobRef.t
+(** Start a [Program Fixpoint] declaration, similar to the above,
+   except it takes a list now. *)
+val add_mutual_definitions :
+     (Constr.t CInfo.t * Constr.t * RetrieveObl.obligation_info) list
+  -> info:Info.t
+  -> uctx:UState.t
+  -> ?tactic:unit Proofview.tactic
+  -> ?reduce:(Constr.t -> Constr.t)
+  -> ?opaque:bool
+  -> ntns:Vernacexpr.decl_notation list
+  -> fixpoint_kind
+  -> unit
 
-(** 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 *)
+(** Implementation of the [Obligation] command *)
+val obligation :
+     int * Names.Id.t option * Constrexpr.constr_expr option
+  -> Genarg.glob_generic_argument option
+  -> Proof.t
 
-type obligation_resolver =
-     Id.t option
-  -> Int.Set.t
-  -> unit Proofview.tactic option
-  -> progress
+(** Implementation of the [Next Obligation] command *)
+val next_obligation :
+  Names.Id.t option -> Genarg.glob_generic_argument option -> Proof.t
 
-type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver}
+(** Implementation of the [Solve Obligation] command *)
+val solve_obligations :
+  Names.Id.t option -> unit Proofview.tactic option -> progress
 
-(** [update_obls prg obls n progress] What does this do? *)
-val update_obls :
-  ProgramDecl.t -> Obligation.t array -> int -> progress
+val solve_all_obligations : unit Proofview.tactic option -> unit
 
-(** Check obligations are properly solved before closing the
-   [what_for] section / module *)
-val check_solved_obligations : what_for:Pp.t -> unit
+(** Number of remaining obligations to be solved for this program *)
+val try_solve_obligation :
+  int -> Names.Id.t option -> unit Proofview.tactic option -> unit
 
-(** { 2 Util }  *)
+val try_solve_obligations :
+  Names.Id.t option -> unit Proofview.tactic option -> unit
 
-val obl_substitution :
-     bool
-  -> Obligation.t array
-  -> Int.Set.t
-  -> (Id.t * (Constr.types * Constr.types)) list
+val show_obligations : ?msg:bool -> Names.Id.t option -> unit
+val show_term : Names.Id.t option -> Pp.t
+val admit_obligations : Names.Id.t option -> unit
 
-val dependencies : Obligation.t array -> int -> Int.Set.t
+val check_program_libraries : unit -> unit
 
 end
 
-(** Creating high-level proofs with an associated constant *)
-module Proof_ending : sig
+(** {6 For internal support, do not use}  *)
 
-  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
-        }
+module Internal : sig
 
-end
+  type constant_obj
 
-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
+  val objConstant : constant_obj Libobject.Dyn.tag
+  val objVariable : unit Libobject.Dyn.tag
 
-  (* Internal; used to initialize non-mutual proofs *)
-  val add_first_thm :
-    info:t
-    -> name:Id.t
-    -> typ:EConstr.t
-    -> impargs:Impargs.manual_implicits
-    -> t
 end
-
-val save_lemma_proved
-  : proof:Proof.t
-  -> info:Info.t
-  -> opaque:opacity_flag
-  -> idopt:Names.lident option
-  -> unit
-
-val save_lemma_admitted :
-     proof:Proof.t
-  -> info:Info.t
-  -> unit
-
-(** Special cases for delayed proofs, in this case we must provide the
-   proof information so the proof won't be forced. *)
-val save_lemma_admitted_delayed :
-     proof:proof_object
-  -> info:Info.t
-  -> unit
-
-val save_lemma_proved_delayed
-  : proof:proof_object
-  -> info:Info.t
-  -> idopt:Names.lident option
-  -> unit
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
deleted file mode 100644
index 83bb1dae71..0000000000
--- a/vernac/declareDef.ml
+++ /dev/null
@@ -1,9 +0,0 @@
-type locality = Declare.locality =
-  | Discharge [@ocaml.deprecated "Use [Declare.Discharge]"]
-  | Global of Declare.import_status [@ocaml.deprecated "Use [Declare.Global]"]
-[@@ocaml.deprecated "Use [Declare.locality]"]
-
-let declare_definition = Declare.declare_definition
-[@@ocaml.deprecated "Use [Declare.declare_definition]"]
-module Hook = Declare.Hook
-[@@ocaml.deprecated "Use [Declare.Hook]"]
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index 80a4de472c..ebec720ce2 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -64,12 +64,12 @@ GRAMMAR EXTEND Gram
       | IDENT "Existential"; n = natural; c = constr_body ->
           { VernacSolveExistential (n,c) }
       | IDENT "Admitted" -> { VernacEndProof Admitted }
-      | IDENT "Qed" -> { VernacEndProof (Proved (Declare.Opaque,None)) }
+      | IDENT "Qed" -> { VernacEndProof (Proved (Opaque,None)) }
       | IDENT "Save"; id = identref ->
-          { VernacEndProof (Proved (Declare.Opaque, Some id)) }
-      | IDENT "Defined" -> { VernacEndProof (Proved (Declare.Transparent,None)) }
+          { VernacEndProof (Proved (Opaque, Some id)) }
+      | IDENT "Defined" -> { VernacEndProof (Proved (Transparent,None)) }
       |	IDENT "Defined"; id=identref ->
-          { VernacEndProof (Proved (Declare.Transparent,Some id)) }
+          { VernacEndProof (Proved (Transparent,Some id)) }
       | IDENT "Restart" -> { VernacRestart }
       | IDENT "Undo" -> { VernacUndo 1 }
       | IDENT "Undo"; n = natural -> { VernacUndo n }
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
deleted file mode 100644
index 10d63ff2ff..0000000000
--- a/vernac/lemmas.ml
+++ /dev/null
@@ -1,130 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Created by Hugo Herbelin from contents related to lemma proofs in
-   file command.ml, Aug 2009 *)
-
-open Util
-
-module NamedDecl = Context.Named.Declaration
-
-(* 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                                       *)
-(************************************************************************)
-
-let initialize_named_context_for_proof () =
-  let sign = Global.named_context () in
-  List.fold_right
-    (fun d signv ->
-      let id = NamedDecl.get_id d in
-      let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in
-      Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
-
-(* Starting a goal *)
-let start_lemma ~name ~poly
-    ?(udecl=UState.default_univ_decl)
-    ?(info=Info.make ()) ?(impargs=[]) sigma c =
-  (* We remove the bodies of variables in the named context marked
-     "opaque", this is a hack tho, see #10446 *)
-  let sign = initialize_named_context_for_proof () in
-  let goals = [ Global.env_of_context sign , c ] in
-  let proof = Declare.start_proof sigma ~name ~udecl ~poly goals in
-  let info = Declare.Info.add_first_thm ~info ~name ~typ:c ~impargs in
-  { proof; info }
-
-(* 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 }
-
-let rec_tac_initializer finite guard thms snl =
-  if finite then
-    match List.map (fun { Declare.Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with
-    | (id,_)::l -> Tactics.mutual_cofix id l 0
-    | _ -> assert false
-  else
-    (* nl is dummy: it will be recomputed at Qed-time *)
-    let nl = match snl with
-     | None -> List.map succ (List.map List.last guard)
-     | Some nl -> nl
-    in match List.map2 (fun { Declare.Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with
-       | (id,n,_)::l -> Tactics.mutual_fix id n l 0
-       | _ -> assert false
-
-let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl =
-  let intro_tac { Declare.Recthm.args; _ } = Tactics.auto_intros_tac args in
-  let init_tac, compute_guard = match recguard with
-  | Some (finite,guard,init_terms) ->
-    let rec_tac = rec_tac_initializer finite guard thms snl in
-    let term_tac =
-      match init_terms with
-      | None ->
-        List.map intro_tac thms
-      | Some init_terms ->
-        (* This is the case for hybrid proof mode / definition
-           fixpoint, where terms for some constants are given with := *)
-        let tacl = List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) init_terms in
-        List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms
-    in
-    Tacticals.New.tclTHENS rec_tac term_tac, guard
-  | None ->
-    let () = match thms with [_] -> () | _ -> assert false in
-    intro_tac (List.hd thms), [] in
-  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
-    (* 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
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
deleted file mode 100644
index 4787a940da..0000000000
--- a/vernac/lemmas.mli
+++ /dev/null
@@ -1,82 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-
-(** {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
-  -> ?impargs:Impargs.manual_implicits
-  -> Evd.evar_map
-  -> EConstr.types
-  -> t
-
-val start_dependent_lemma
-  :  name:Id.t
-  -> poly:bool
-  -> ?udecl:UState.universe_decl
-  -> ?info:Info.t
-  -> Proofview.telescope
-  -> t
-
-type lemma_possible_guards = int list list
-
-(** Pretty much internal, used by the Lemma / Fixpoint vernaculars *)
-val start_lemma_with_initialization
-  :  ?hook:Declare.Hook.t
-  -> poly:bool
-  -> scope:Declare.locality
-  -> kind:Decls.logical_kind
-  -> udecl:UState.universe_decl
-  -> Evd.evar_map
-  -> (bool * 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
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
deleted file mode 100644
index a8eac8fd2d..0000000000
--- a/vernac/obligations.ml
+++ /dev/null
@@ -1,417 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Printf
-open Names
-open Pp
-open Util
-
-(* For the records fields, opens should go away one these types are private *)
-open Declare.Obls
-open Declare.Obls.Obligation
-open Declare.Obls.ProgramDecl
-
-let reduce c =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota env sigma (EConstr.of_constr c))
-
-let explain_no_obligations = function
-    Some ident -> str "No obligations for program " ++ Id.print ident
-  | None -> str "No obligations remaining"
-
-module Error = struct
-
-  let no_obligations n =
-    CErrors.user_err (explain_no_obligations n)
-
-  let ambiguous_program id ids =
-    CErrors.user_err
-      Pp.(str "More than one program with unsolved obligations: " ++ prlist Id.print ids
-          ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print id ++ str "\"")
-
-  let unknown_obligation num =
-    CErrors.user_err (Pp.str (sprintf "Unknown obligation number %i" (succ num)))
-
-  let already_solved num =
-    CErrors.user_err
-      ( str "Obligation" ++ spc () ++ int num ++ str "already" ++ spc ()
-        ++ str "solved." )
-
-  let depends num rem =
-    CErrors.user_err
-      ( str "Obligation " ++ int num
-        ++ str " depends on obligation(s) "
-        ++ pr_sequence (fun x -> int (succ x)) rem)
-
-end
-
-let default_tactic = ref (Proofview.tclUNIT ())
-
-let evar_of_obligation o = Evd.make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
-
-let subst_deps expand obls deps t =
-  let osubst = Declare.Obls.obl_substitution expand obls deps in
-    (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
-
-let subst_deps_obl obls obl =
-  let t' = subst_deps true obls obl.obl_deps obl.obl_type in
-  Obligation.set_type ~typ:t' obl
-
-open Evd
-
-let is_defined obls x = not (Option.is_empty obls.(x).obl_body)
-
-let deps_remaining obls deps =
-  Int.Set.fold
-    (fun x acc ->
-      if is_defined obls x then acc
-      else x :: acc)
-    deps []
-
-let goal_kind = Decls.(IsDefinition Definition)
-let goal_proof_kind = Decls.(IsProof Lemma)
-
-let kind_of_obligation o =
-  match o with
-  | Evar_kinds.Define false
-  | Evar_kinds.Expand -> goal_kind
-  | _ -> goal_proof_kind
-
-(* Solve an obligation using tactics, return the corresponding proof term *)
-let warn_solve_errored =
-  CWarnings.create ~name:"solve_obligation_error" ~category:"tactics"
-    (fun err ->
-      Pp.seq
-        [ str "Solve Obligations tactic returned error: "
-        ; err
-        ; fnl ()
-        ; str "This will become an error in the future" ])
-
-let solve_by_tac ?loc name evi t poly uctx =
-  (* the status is dropped. *)
-  try
-    let env = Global.env () in
-    let body, types, _univs, _, uctx =
-      Declare.build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in
-    Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body);
-    Some (body, types, uctx)
-  with
-  | Refiner.FailError (_, s) as exn ->
-    let _ = Exninfo.capture exn in
-    CErrors.user_err ?loc ~hdr:"solve_obligation" (Lazy.force s)
-  (* If the proof is open we absorb the error and leave the obligation open *)
-  | Proof.OpenProof _ ->
-    None
-  | e when CErrors.noncritical e ->
-    let err = CErrors.print e in
-    warn_solve_errored ?loc err;
-    None
-
-let get_unique_prog prg =
-  match State.get_unique_open_prog prg with
-  | Ok prg -> prg
-  | Error [] ->
-    Error.no_obligations None
-  | Error ((id :: _) as ids) ->
-    Error.ambiguous_program id ids
-
-let rec solve_obligation prg num tac =
-  let user_num = succ num in
-  let { obls; remaining=rem } = prg.prg_obligations in
-  let obl = obls.(num) in
-  let remaining = deps_remaining obls obl.obl_deps in
-  let () =
-    if not (Option.is_empty obl.obl_body)
-    then Error.already_solved user_num;
-    if not (List.is_empty remaining)
-    then Error.depends user_num remaining
-  in
-  let obl = subst_deps_obl obls obl in
-  let scope = Declare.(Global Declare.ImportNeedQualified) in
-  let kind = kind_of_obligation (snd obl.obl_status) in
-  let evd = Evd.from_ctx prg.prg_ctx in
-  let evd = Evd.update_sigma_env evd (Global.env ()) in
-  let auto n oblset tac = auto_solve_obligations n ~oblset tac in
-  let proof_ending =
-    Declare.Proof_ending.End_obligation
-      {Declare.Obls.name = prg.prg_name; num; auto}
-  in
-  let info = Lemmas.Info.make ~proof_ending ~scope ~kind () in
-  let poly = prg.prg_poly in
-  let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in
-  let lemma = fst @@ Lemmas.by !default_tactic lemma in
-  let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in
-  lemma
-
-and obligation (user_num, name, typ) tac =
-  let num = pred user_num in
-  let prg = get_unique_prog name in
-  let { obls; remaining } = prg.prg_obligations in
-  if num >= 0 && num < Array.length obls then
-    let obl = obls.(num) in
-    match obl.obl_body with
-    | None -> solve_obligation prg num tac
-    | Some r -> Error.already_solved num
-  else Error.unknown_obligation num
-
-and solve_obligation_by_tac prg obls i tac =
-  let obl = obls.(i) in
-    match obl.obl_body with
-    | Some _ -> None
-    | None ->
-      if List.is_empty (deps_remaining obls obl.obl_deps) then
-        let obl = subst_deps_obl obls obl in
-        let tac =
-          match tac with
-          | Some t -> t
-          | None ->
-            match obl.obl_tac with
-            | Some t -> t
-            | None -> !default_tactic
-        in
-        let evd = Evd.from_ctx prg.prg_ctx in
-        let evd = Evd.update_sigma_env evd (Global.env ()) in
-        match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac
-                prg.prg_poly (Evd.evar_universe_context evd) with
-        | None -> None
-        | Some (t, ty, uctx) ->
-          let prg = ProgramDecl.set_uctx ~uctx prg in
-          (* Why is uctx not used above? *)
-          let def, obl' = declare_obligation prg obl ~body:t ~types:ty ~uctx in
-          obls.(i) <- obl';
-          if def && not prg.prg_poly then (
-            (* Declare the term constraints with the first obligation only *)
-            let uctx_global = UState.from_env (Global.env ()) in
-            let uctx = UState.merge_subst uctx_global (UState.subst uctx) in
-            Some (ProgramDecl.set_uctx ~uctx prg))
-          else Some prg
-      else None
-
-and solve_prg_obligations prg ?oblset tac =
-  let { obls; remaining } = prg.prg_obligations in
-  let rem = ref remaining in
-  let obls' = Array.copy obls in
-  let set = ref Int.Set.empty in
-  let p = match oblset with
-    | None -> (fun _ -> true)
-    | Some s -> set := s;
-      (fun i -> Int.Set.mem i !set)
-  in
-  let (), prg =
-    Array.fold_left_i
-      (fun i ((), prg) x ->
-        if p i then (
-          match solve_obligation_by_tac prg obls' i tac with
-          | None -> (), prg
-          | Some prg ->
-            let deps = dependencies obls i in
-            set := Int.Set.union !set deps;
-            decr rem;
-            (), prg)
-        else (), prg)
-      ((), prg) obls'
-  in
-  update_obls prg obls' !rem
-
-and solve_obligations n tac =
-  let prg = get_unique_prog n in
-    solve_prg_obligations prg tac
-
-and solve_all_obligations tac =
-  State.fold ~init:() ~f:(fun k v () ->
-      let _ = solve_prg_obligations v tac in ())
-
-and try_solve_obligation n prg tac =
-  let prg = get_unique_prog prg in
-  let {obls; remaining } = prg.prg_obligations in
-  let obls' = Array.copy obls in
-  match solve_obligation_by_tac prg obls' n tac with
-  | Some prg' ->
-    let _r = update_obls prg' obls' (pred remaining) in
-    ()
-  | None -> ()
-
-and try_solve_obligations n tac =
-  let _ = solve_obligations n tac in
-  ()
-
-and auto_solve_obligations n ?oblset tac : progress =
-  Flags.if_verbose Feedback.msg_info
-    (str "Solving obligations automatically...");
-  let prg = get_unique_prog n in
-  solve_prg_obligations prg ?oblset tac
-
-open Pp
-
-let show_single_obligation i n obls x =
-  let x = subst_deps_obl obls x in
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  let msg =
-    str "Obligation" ++ spc ()
-    ++ int (succ i)
-    ++ spc () ++ str "of" ++ spc () ++ Id.print n ++ str ":" ++ spc ()
-    ++ hov 1 (Printer.pr_constr_env env sigma x.obl_type
-              ++ str "." ++ fnl ()) in
-  Feedback.msg_info msg
-
-let show_obligations_of_prg ?(msg = true) prg =
-  let n = prg.prg_name in
-  let {obls; remaining} = prg.prg_obligations in
-  let showed = ref 5 in
-    if msg then Feedback.msg_info (int remaining ++ str " obligation(s) remaining: ");
-    Array.iteri
-      (fun i x ->
-         match x.obl_body with
-         | None ->
-           if !showed > 0 then begin
-             decr showed;
-             show_single_obligation i n obls x
-           end
-         | Some _ -> ())
-      obls
-
-let show_obligations ?(msg = true) n =
-  let progs =
-    match n with
-    | None ->
-      State.all ()
-    | Some n ->
-      (match State.find n with
-       | Some prg -> [prg]
-       | None -> Error.no_obligations (Some n))
-  in
-  List.iter (fun x -> show_obligations_of_prg ~msg x) progs
-
-let show_term n =
-  let prg = get_unique_prog n in
-  let n = prg.prg_name in
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  Id.print n ++ spc () ++ str ":" ++ spc ()
-  ++ Printer.pr_constr_env env sigma prg.prg_type
-  ++ spc () ++ str ":=" ++ fnl ()
-  ++ Printer.pr_constr_env env sigma prg.prg_body
-
-let msg_generating_obl name obls =
-  let len = Array.length obls in
-  let info = Id.print name ++ str " has type-checked" in
-  Feedback.msg_info
-    (if len = 0 then info ++ str "."
-     else
-       info ++ str ", generating " ++ int len ++
-       str (String.plural len " obligation"))
-
-let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl)
-    ?(impargs = []) ~poly
-    ?(scope = Declare.Global Declare.ImportDefaultBehavior)
-    ?(kind = Decls.Definition) ?tactic ?(reduce = reduce) ?hook
-    ?(opaque = false) obls =
-  let prg = ProgramDecl.make ~opaque name ~udecl term t ~uctx [] None [] obls ~impargs ~poly ~scope ~kind reduce ?hook in
-  let {obls;_} = prg.prg_obligations in
-  if Int.equal (Array.length obls) 0 then (
-    Flags.if_verbose (msg_generating_obl name) obls;
-    let cst = Declare.Obls.declare_definition prg in
-    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 ->
-      Flags.if_verbose (show_obligations ~msg:false) (Some name);
-      res
-    | _ -> res
-
-let add_mutual_definitions l ~uctx ?(udecl = UState.default_univ_decl)
-    ?tactic ~poly ?(scope = Declare.Global Declare.ImportDefaultBehavior)
-    ?(kind = Decls.Definition) ?(reduce = reduce) ?hook ?(opaque = false)
-    notations fixkind =
-  let deps = List.map (fun ({Declare.Recthm.name; _}, _, _) -> name) l in
-  let pm =
-    List.fold_left
-      (fun () ({Declare.Recthm.name; typ; impargs; _}, b, obls) ->
-        let prg =
-          ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps
-            (Some fixkind) notations obls ~impargs ~poly ~scope ~kind reduce
-            ?hook
-        in
-        State.add name prg)
-      () l
-  in
-  let pm, _defined =
-    List.fold_left
-      (fun (pm, finished) x ->
-        if finished then (pm, finished)
-        else
-          let res = auto_solve_obligations (Some x) tactic in
-          match res with
-          | Defined _ ->
-            (* If one definition is turned into a constant,
-               the whole block is defined. *)
-            (pm, true)
-          | _ -> (pm, false))
-      (pm, false) deps
-  in
-  pm
-
-let admit_prog prg =
-  let {obls; remaining} = prg.prg_obligations in
-  let obls = Array.copy obls in
-    Array.iteri
-      (fun i x ->
-        match x.obl_body with
-        | None ->
-            let x = subst_deps_obl obls x in
-            let ctx = UState.univ_entry ~poly:false prg.prg_ctx in
-            let kn = Declare.declare_constant ~name:x.obl_name ~local:Declare.ImportNeedQualified
-              (Declare.ParameterEntry (None, (x.obl_type, ctx), None)) ~kind:Decls.(IsAssumption Conjectural)
-            in
-              Declare.assumption_message x.obl_name;
-              obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x
-        | Some _ -> ())
-      obls;
-  Declare.Obls.update_obls prg obls 0
-
-(* get_any_prog *)
-let rec admit_all_obligations () =
-  let prg = State.first_pending () in
-  match prg with
-  | None -> ()
-  | Some prg ->
-    let _prog = admit_prog prg in
-    admit_all_obligations ()
-
-let admit_obligations n =
-  match n with
-  | None -> admit_all_obligations ()
-  | Some _ ->
-    let prg = get_unique_prog n in
-    let _ = admit_prog prg in
-    ()
-
-let next_obligation n tac =
-  let prg = match n with
-    | None -> State.first_pending () |> Option.get
-    | Some _ -> get_unique_prog n
-  in
-  let {obls; remaining} = prg.prg_obligations in
-  let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
-  let i = match Array.findi is_open obls with
-    | Some i -> i
-    | None -> CErrors.anomaly (Pp.str "Could not find a solvable obligation.")
-  in
-  solve_obligation prg i tac
-
-let check_program_libraries () =
-  Coqlib.check_required_library Coqlib.datatypes_module_name;
-  Coqlib.check_required_library ["Coq";"Init";"Specif"];
-  Coqlib.check_required_library ["Coq";"Program";"Tactics"]
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
deleted file mode 100644
index c21951373b..0000000000
--- a/vernac/obligations.mli
+++ /dev/null
@@ -1,135 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Constr
-
-(** Coq's Program mode support. This mode extends declarations of
-   constants and fixpoints with [Program Definition] and [Program
-   Fixpoint] to support incremental construction of terms using
-   delayed proofs, called "obligations"
-
-    The mode also provides facilities for managing and auto-solving
-   sets of obligations.
-
-    The basic code flow of programs/obligations is as follows:
-
-    - [add_definition] / [add_mutual_definitions] are called from the
-   respective [Program] vernacular command interpretation; at this
-   point the only extra work we do is to prepare the new definition
-   [d] using [RetrieveObl], which consists in turning unsolved evars
-   into obligations. [d] is not sent to the kernel yet, as it is not
-   complete and cannot be typchecked, but saved in a special
-   data-structure. Auto-solving of obligations is tried at this stage
-   (see below)
-
-   - [next_obligation] will retrieve the next obligation
-   ([RetrieveObl] sorts them by topological order) and will try to
-   solve it. When all obligations are solved, the original constant
-   [d] is grounded and sent to the kernel for addition to the global
-   environment. Auto-solving of obligations is also triggered on
-   obligation completion.
-
-{2} Solving of obligations: Solved obligations are stored as regular
-   global declarations in the global environment, usually with name
-   [constant_obligation_number] where [constant] is the original
-   [constant] and [number] is the corresponding (internal) number.
-
-   Solving an obligation can trigger a bit of a complex cascaded
-   callback path; closing an obligation can indeed allow all other
-   obligations to be closed, which in turn may trigged the declaration
-   of the original constant. Care must be taken, as this can modify
-   [Global.env] in arbitrarily ways. Current code takes some care to
-   refresh the [env] in the proper boundaries, but the invariants
-   remain delicate.
-
-{2} Saving of obligations: as open obligations use the regular proof
-   mode, a `Qed` will call `Lemmas.save_lemma` first. For this reason
-   obligations code is split in two: this file, [Obligations], taking
-   care of the top-level vernac commands, and [DeclareObl], which is
-   called by `Lemmas` to close an obligation proof and eventually to
-   declare the top-level [Program]ed constant.
-
-    There is little obligations-specific code in [DeclareObl], so
-   eventually that file should be integrated in the regular [Declare]
-   path, as it gains better support for "dependent_proofs".
-
- *)
-
-val default_tactic : unit Proofview.tactic ref
-
-(** Start a [Program Definition c] proof. [uctx] [udecl] [impargs]
-   [kind] [scope] [poly] etc... come from the interpretation of the
-   vernacular; `obligation_info` was generated by [RetrieveObl] It
-   will return whether all the obligations were solved; if so, it will
-   also register [c] with the kernel. *)
-val add_definition :
-     name:Names.Id.t
-  -> ?term:constr
-  -> types
-  -> uctx:UState.t
-  -> ?udecl:UState.universe_decl (** Universe binders and constraints *)
-  -> ?impargs:Impargs.manual_implicits
-  -> poly:bool
-  -> ?scope:Declare.locality
-  -> ?kind:Decls.definition_object_kind
-  -> ?tactic:unit Proofview.tactic
-  -> ?reduce:(constr -> constr)
-  -> ?hook:Declare.Hook.t
-  -> ?opaque:bool
-  -> RetrieveObl.obligation_info
-  -> Declare.Obls.progress
-
-(* XXX: unify with MutualEntry *)
-
-(** Start a [Program Fixpoint] declaration, similar to the above,
-   except it takes a list now. *)
-val add_mutual_definitions :
-     (Declare.Recthm.t * Constr.t * RetrieveObl.obligation_info) list
-  -> uctx:UState.t
-  -> ?udecl:UState.universe_decl (** Universe binders and constraints *)
-  -> ?tactic:unit Proofview.tactic
-  -> poly:bool
-  -> ?scope:Declare.locality
-  -> ?kind:Decls.definition_object_kind
-  -> ?reduce:(constr -> constr)
-  -> ?hook:Declare.Hook.t
-  -> ?opaque:bool
-  -> Vernacexpr.decl_notation list
-  -> Declare.Obls.fixpoint_kind
-  -> unit
-
-(** Implementation of the [Obligation] command *)
-val obligation :
-     int * Names.Id.t option * Constrexpr.constr_expr option
-  -> Genarg.glob_generic_argument option
-  -> Lemmas.t
-
-(** Implementation of the [Next Obligation] command *)
-val next_obligation :
-  Names.Id.t option -> Genarg.glob_generic_argument option -> Lemmas.t
-
-(** Implementation of the [Solve Obligation] command *)
-val solve_obligations :
-  Names.Id.t option -> unit Proofview.tactic option -> Declare.Obls.progress
-
-val solve_all_obligations : unit Proofview.tactic option -> unit
-
-(** Number of remaining obligations to be solved for this program *)
-val try_solve_obligation :
-  int -> Names.Id.t option -> unit Proofview.tactic option -> unit
-
-val try_solve_obligations :
-  Names.Id.t option -> unit Proofview.tactic option -> unit
-
-val show_obligations : ?msg:bool -> Names.Id.t option -> unit
-val show_term : Names.Id.t option -> Pp.t
-val admit_obligations : Names.Id.t option -> unit
-
-val check_program_libraries : unit -> unit
diff --git a/vernac/pfedit.ml b/vernac/pfedit.ml
deleted file mode 100644
index 150311ffaa..0000000000
--- a/vernac/pfedit.ml
+++ /dev/null
@@ -1,19 +0,0 @@
-(* Compat API / *)
-let get_current_context = Declare.get_current_context
-[@@ocaml.deprecated "Use [Declare.get_current_context]"]
-let solve = Proof.solve
-[@@ocaml.deprecated "Use [Proof.solve]"]
-let by = Declare.by
-[@@ocaml.deprecated "Use [Declare.by]"]
-let refine_by_tactic = Proof.refine_by_tactic
-[@@ocaml.deprecated "Use [Proof.refine_by_tactic]"]
-
-(* We don't want to export this anymore, but we do for now *)
-let build_by_tactic ?side_eff env ~uctx ~poly ~typ tac =
-  let b, t, _unis, safe, uctx =
-    Declare.build_by_tactic ?side_eff env ~uctx ~poly ~typ tac in
-  b, t, safe, uctx
-[@@ocaml.deprecated "Use [Proof.build_by_tactic]"]
-
-let build_constant_by_tactic = Declare.build_constant_by_tactic [@ocaml.warning "-3"]
-[@@ocaml.deprecated "Use [Proof.build_constant_by_tactic]"]
diff --git a/vernac/proof_global.ml b/vernac/proof_global.ml
deleted file mode 100644
index 0c5bc39020..0000000000
--- a/vernac/proof_global.ml
+++ /dev/null
@@ -1,13 +0,0 @@
-(* compatibility module; can be removed once we agree on the API *)
-
-type t = Declare.Proof.t
-[@@ocaml.deprecated "Use [Declare.Proof.t]"]
-let map_proof = Declare.Proof.map_proof
-[@@ocaml.deprecated "Use [Declare.Proof.map_proof]"]
-let get_proof = Declare.Proof.get_proof
-[@@ocaml.deprecated "Use [Declare.Proof.get_proof]"]
-
-type opacity_flag = Declare.opacity_flag =
-  | Opaque [@ocaml.deprecated "Use [Declare.Opaque]"]
-  | Transparent [@ocaml.deprecated "Use [Declare.Transparent]"]
-[@@ocaml.deprecated "Use [Declare.opacity_flag]"]
diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml
index eb0e1fb795..534c358a3f 100644
--- a/vernac/recLemmas.ml
+++ b/vernac/recLemmas.ml
@@ -16,9 +16,9 @@ module RelDecl = Context.Rel.Declaration
 
 let find_mutually_recursive_statements sigma thms =
     let n = List.length thms in
-    let inds = List.map (fun (id,(t,impls)) ->
-      let (hyps,ccl) = EConstr.decompose_prod_assum sigma t in
-      let x = (id,(t,impls)) in
+    let inds = List.map (fun x ->
+      let typ = Declare.CInfo.get_typ x in
+      let (hyps,ccl) = EConstr.decompose_prod_assum sigma typ in
       let whnf_hyp_hds = EConstr.map_rel_context_in_env
         (fun env c -> fst (Reductionops.whd_all_stack env sigma c))
         (Global.env()) hyps in
@@ -89,14 +89,23 @@ let find_mutually_recursive_statements sigma thms =
     in
     (finite,guard,None), ordered_inds
 
-let look_for_possibly_mutual_statements sigma = function
-  | [id,(t,impls)] ->
+type mutual_info =
+  | NonMutual of EConstr.t Declare.CInfo.t
+  | Mutual of
+      { mutual_info : Declare.Proof.mutual_info
+      ; cinfo : EConstr.t Declare.CInfo.t list
+      ; possible_guards : int list
+      }
+
+let look_for_possibly_mutual_statements sigma thms : mutual_info =
+  match thms with
+  | [thm] ->
       (* One non recursively proved theorem *)
-      None,[id,(t,impls)],None
+    NonMutual thm
   | _::_ as thms ->
     (* More than one statement and/or an explicit decreasing mark: *)
     (* we look for a common inductive hyp or a common coinductive conclusion *)
     let recguard,ordered_inds = find_mutually_recursive_statements sigma thms in
-    let thms = List.map pi2 ordered_inds in
-    Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds)
+    let cinfo = List.map pi2 ordered_inds in
+    Mutual { mutual_info = recguard; cinfo; possible_guards = List.map (fun (_,_,i) -> succ i) ordered_inds }
   | [] -> CErrors.anomaly (Pp.str "Empty list of theorems.")
diff --git a/vernac/recLemmas.mli b/vernac/recLemmas.mli
index 1a697c1e88..93aae29b18 100644
--- a/vernac/recLemmas.mli
+++ b/vernac/recLemmas.mli
@@ -8,8 +8,15 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+type mutual_info =
+  | NonMutual of EConstr.t Declare.CInfo.t
+  | Mutual of
+      { mutual_info : Declare.Proof.mutual_info
+      ; cinfo : EConstr.t Declare.CInfo.t list
+      ; possible_guards : int list
+      }
+
 val look_for_possibly_mutual_statements
   :  Evd.evar_map
-  -> ('a * (EConstr.t * 'b)) list
-  -> (bool * int list list * 'c option) option *
-     ('a * (EConstr.t * 'b)) list * int list option
+  -> EConstr.t Declare.CInfo.t list
+  -> mutual_info
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 1cad052bce..23dde0dd29 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -20,11 +20,9 @@ ComHints
 Canonical
 RecLemmas
 Library
-Lemmas
 ComCoercion
 Auto_ind_decl
 Indschemes
-Obligations
 ComDefinition
 Classes
 ComPrimitive
@@ -45,6 +43,3 @@ ComArguments
 Vernacentries
 Vernacstate
 Vernacinterp
-Proof_global
-Pfedit
-DeclareDef
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9a1d935928..d44e4babf4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -34,12 +34,12 @@ let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
 let get_current_or_global_context ~pstate =
   match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
-  | Some p -> Declare.get_current_context p
+  | Some p -> Declare.Proof.get_current_context p
 
 let get_goal_or_global_context ~pstate glnum =
   match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
-  | Some p -> Declare.get_goal_context p glnum
+  | Some p -> Declare.Proof.get_goal_context p glnum
 
 let cl_of_qualid = function
   | FunClass -> Coercionops.CL_FUN
@@ -84,7 +84,7 @@ let with_module_locality ~atts f =
 
 let with_def_attributes ~atts f =
   let atts = DefAttributes.parse atts in
-  if atts.DefAttributes.program then Obligations.check_program_libraries ();
+  if atts.DefAttributes.program then Declare.Obls.check_program_libraries ();
   f ~atts
 
 (*******************)
@@ -94,8 +94,8 @@ 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 sigma, _ = Declare.get_current_context pstate in
+    let p = Declare.Proof.get pstate in
+    let sigma, _ = Declare.Proof.get_current_context pstate in
     let pprf = Proof.partial_proof p in
     (* In the absence of an environment explicitly attached to the
        proof and on top of which side effects of the proof would be pushed, ,
@@ -466,12 +466,12 @@ let vernac_custom_entry ~module_local s =
 let check_name_freshness locality {CAst.loc;v=id} : unit =
   (* We check existence here: it's a bit late at Qed time *)
   if Nametab.exists_cci (Lib.make_path id) || Termops.is_section_variable id ||
-     locality <> Declare.Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
+     locality <> Locality.Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
   then
     user_err ?loc  (Id.print id ++ str " already exists.")
 
 let program_inference_hook env sigma ev =
-  let tac = !Obligations.default_tactic in
+  let tac = !Declare.Obls.default_tactic in
   let evi = Evd.find sigma ev in
   let evi = Evarutil.nf_evar_info sigma evi in
   let env = Evd.evar_filtered_env env evi in
@@ -490,38 +490,54 @@ let program_inference_hook env sigma ev =
     user_err Pp.(str "The statement obligations could not be resolved \
                       automatically, write a statement definition first.")
 
+(* XXX: Interpretation of lemma command, duplication with ComFixpoint
+   / ComDefinition ? *)
+let interp_lemma ~program_mode ~flags ~scope env0 evd thms =
+  let inference_hook = if program_mode then Some program_inference_hook else None in
+  List.fold_left_map (fun evd ((id, _), (bl, t)) ->
+      let evd, (impls, ((env, ctx), imps)) =
+        Constrintern.interp_context_evars ~program_mode env0 evd bl
+      in
+      let evd, (t', imps') = Constrintern.interp_type_evars_impls ~flags ~impls env evd t in
+      let flags = Pretyping.{ all_and_fail_flags with program_mode } in
+      let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in
+      let ids = List.map Context.Rel.Declaration.get_name ctx in
+      check_name_freshness scope id;
+      let thm = Declare.CInfo.make ~name:id.CAst.v ~typ:(EConstr.it_mkProd_or_LetIn t' ctx)
+          ~args:ids ~impargs:(imps @ imps') () in
+      evd, thm)
+    evd thms
+
+(* Checks done in start_lemma_com *)
+let post_check_evd ~udecl ~poly evd =
+  let () =
+    if not UState.(udecl.univdecl_extensible_instance &&
+                   udecl.univdecl_extensible_constraints) then
+      ignore (Evd.check_univ_decl ~poly evd udecl)
+  in
+  if poly then evd
+  else (* We fix the variables to ensure they won't be lowered to Set *)
+    Evd.fix_undefined_variables evd
+
 let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   let env0 = Global.env () in
   let flags = Pretyping.{ all_no_fail_flags with program_mode } in
   let decl = fst (List.hd thms) in
   let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
-  let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) ->
-    let evd, (impls, ((env, ctx), imps)) =
-      Constrintern.interp_context_evars ~program_mode env0 evd bl
-    in
-    let evd, (t', imps') = Constrintern.interp_type_evars_impls ~flags ~impls env evd t in
-    let flags = Pretyping.{ all_and_fail_flags with program_mode } in
-    let inference_hook = if program_mode then Some program_inference_hook else None in
-    let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in
-    let ids = List.map Context.Rel.Declaration.get_name ctx in
-    check_name_freshness scope id;
-    evd, (id.CAst.v, (EConstr.it_mkProd_or_LetIn t' ctx, (ids, imps @ imps'))))
-      evd thms in
-  let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in
+  let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in
+  let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in
   let evd = Evd.minimize_universes evd in
-  let thms = List.map (fun (name, (typ, (args, impargs))) ->
-      { Declare.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in
-  let () =
-    let open UState in
-    if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then
-       ignore (Evd.check_univ_decl ~poly evd udecl)
-  in
-  let evd =
-    if poly then evd
-    else (* We fix the variables to ensure they won't be lowered to Set *)
-      Evd.fix_undefined_variables evd
-  in
-  Lemmas.start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
+  match mut_analysis with
+  | RecLemmas.NonMutual thm ->
+    let thm = Declare.CInfo.to_constr evd thm in
+    let evd = post_check_evd ~udecl ~poly evd in
+    let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
+    Declare.Proof.start_with_initialization ~info ~cinfo:thm evd
+  | RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } ->
+    let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in
+    let evd = post_check_evd ~udecl ~poly evd in
+    let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
+    Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards)
 
 let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
 | Coercion ->
@@ -548,7 +564,6 @@ let vernac_definition_name lid local =
          CAst.make ?loc (fresh_name_for_anonymous_theorem ())
     | { v = Name.Name n; loc } -> CAst.make ?loc n in
   let () =
-    let open Declare in
     match local with
     | Discharge -> Dumpglob.dump_definition lid true "var"
     | Global _ -> Dumpglob.dump_definition lid false "def"
@@ -577,6 +592,7 @@ let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt
       let sigma = Evd.from_env env in
       Some (snd (Hook.get f_interp_redexp env sigma r)) in
   if program_mode then
+    let kind = Decls.IsDefinition kind in
     ComDefinition.do_definition_program ~name:name.v
       ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook
   else
@@ -595,15 +611,16 @@ let vernac_start_proof ~atts kind l =
 
 let vernac_end_proof ~lemma = let open Vernacexpr in function
   | Admitted ->
-    Lemmas.save_lemma_admitted ~lemma
+    Declare.Proof.save_admitted ~proof:lemma
   | Proved (opaque,idopt) ->
-    Lemmas.save_lemma_proved ~lemma ~opaque ~idopt
+    let _ : Names.GlobRef.t list = Declare.Proof.save ~proof:lemma ~opaque ~idopt
+    in ()
 
 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.Proof.by (Tactics.exact_proof c) lemma in
+  let _ : _ list = Declare.Proof.save ~proof:lemma ~opaque:Opaque ~idopt:None in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
@@ -613,8 +630,8 @@ let vernac_assumption ~atts discharge kind l nl =
     if Dumpglob.dump () then
       List.iter (fun (lid, _) ->
           match scope with
-            | Declare.Global _ -> Dumpglob.dump_definition lid false "ax"
-            | Declare.Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
+            | Global _ -> Dumpglob.dump_definition lid false "ax"
+            | Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
   ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
 
 let is_polymorphic_inductive_cumulativity =
@@ -1187,7 +1204,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 +1217,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
@@ -1602,8 +1619,8 @@ let get_current_context_of_args ~pstate =
     let env = Global.env () in Evd.(from_env env, env)
   | Some lemma ->
     function
-    | Some n -> Declare.get_goal_context lemma n
-    | None -> Declare.get_current_context lemma
+    | Some n -> Declare.Proof.get_goal_context lemma n
+    | None -> Declare.Proof.get_current_context lemma
 
 let query_command_selector ?loc = function
   | None -> None
@@ -1668,7 +1685,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
@@ -1703,7 +1720,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
     let natureofid = match decl with
                      | LocalAssum _ -> "Hypothesis"
                      | LocalDef (_,bdy,_) ->"Constant (let in)" in
-    let sigma, env = Declare.get_current_context pstate in
+    let sigma, env = Declare.Proof.get_current_context pstate in
     v 0 (Id.print id ++ str":" ++ pr_econstr_env env sigma (NamedDecl.get_type decl) ++ fnl() ++ fnl()
          ++ str natureofid ++ str " of the goal context.")
   with (* fallback to globals *)
@@ -1747,7 +1764,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 +1850,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 +1861,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 +1880,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 +1890,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 +1912,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 +1924,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..1b977b8e10 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
@@ -213,21 +213,23 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) =
 *)
 
 (* Interpreting a possibly delayed proof *)
-let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option =
+let interp_qed_delayed ~proof ~pinfo ~st pe : Vernacstate.LemmaStack.t option =
   let stack = st.Vernacstate.lemmas in
   let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
   let () = match pe with
     | Admitted ->
-      Declare.save_lemma_admitted_delayed ~proof ~info
+      Declare.Proof.save_lemma_admitted_delayed ~proof ~pinfo
     | Proved (_,idopt) ->
-      Declare.save_lemma_proved_delayed ~proof ~info ~idopt in
+      let _ : _ list = Declare.Proof.save_lemma_proved_delayed ~proof ~pinfo ~idopt in
+      ()
+  in
   stack
 
-let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } =
+let interp_qed_delayed_control ~proof ~pinfo ~st ~control { CAst.loc; v=pe } =
   let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in
   List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
     control
-    (fun ~st -> interp_qed_delayed ~proof ~info ~st pe)
+    (fun ~st -> interp_qed_delayed ~proof ~pinfo ~st pe)
     ~st
 
 (* General interp with management of state *)
@@ -257,6 +259,6 @@ let interp_gen ~verbosely ~st ~interp_fn cmd =
 let interp ?(verbosely=true) ~st cmd =
   interp_gen ~verbosely ~st ~interp_fn:interp_control cmd
 
-let interp_qed_delayed_proof ~proof ~info ~st ~control pe : Vernacstate.t =
+let interp_qed_delayed_proof ~proof ~pinfo ~st ~control pe : Vernacstate.t =
   interp_gen ~verbosely:false ~st
-    ~interp_fn:(interp_qed_delayed_control ~proof ~info ~control) pe
+    ~interp_fn:(interp_qed_delayed_control ~proof ~pinfo ~control) pe
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index e3e708e87d..84d3256c9f 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -14,8 +14,8 @@ val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control ->
 (** Execute a Qed but with a proof_object which may contain a delayed
    proof and won't be forced *)
 val interp_qed_delayed_proof
-  :  proof:Declare.proof_object
-  -> info:Lemmas.Info.t
+  :  proof:Declare.Proof.proof_object
+  -> pinfo:Declare.Proof.Proof_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..17c89897fe 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,14 +43,14 @@ 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.get tgt) src
 
-  let copy_info ~src ~tgt =
+  let copy_info ~(src : t) ~(tgt : t) =
     let (ps, psl), (ts,tsl) = src, tgt in
     copy_info ps ts,
     List.map2 (fun op p -> copy_info op p) psl tsl
@@ -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,43 +133,42 @@ 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.proof_object * Declare.Proof.Proof_info.t
 
-  let return_proof () = cc return_proof
-  let return_partial_proof () = cc return_partial_proof
+  let return_proof () = cc Declare.Proof.return_proof
+  let return_partial_proof () = cc Declare.Proof.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.Proof.close_future_proof ~feedback_id pt pf,
+                  Declare.Proof.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.Proof.close_proof ~opaque ~keep_body_ucst_separate pt,
+                  Declare.Proof.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
+  let get_current_context () = cc Declare.Proof.get_current_context
 
   let get_all_proof_names () =
     try cc_stack LemmaStack.get_all_proof_names
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index fb6d8b6db6..c99db34873 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
 
@@ -65,16 +65,16 @@ module Declare : sig
   val with_current_proof :
       (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
 
-  val return_proof : unit -> Declare.closed_proof_output
-  val return_partial_proof : unit -> Declare.closed_proof_output
+  val return_proof : unit -> Declare.Proof.closed_proof_output
+  val return_partial_proof : unit -> Declare.Proof.closed_proof_output
 
-  type closed_proof = Declare.proof_object * Lemmas.Info.t
+  type closed_proof = Declare.Proof.proof_object * Declare.Proof.Proof_info.t
 
   val close_future_proof :
     feedback_id:Stateid.t ->
-    Declare.closed_proof_output Future.computation -> closed_proof
+    Declare.Proof.closed_proof_output Future.computation -> closed_proof
 
-  val close_proof : opaque:Declare.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof
+  val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof
 
   val discard_all : unit -> unit
   val update_global_env : unit -> unit