[declare] Reify Proof.t API into the Proof module.

This is in preparation for the next commit which will clean-up the
current API flow in `Declare`.

15 files changed, 128 insertions, 124 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index dee407bbe4..d24d968c01 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -286,7 +286,7 @@ END
 VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
 | ![ proof_query ] [ "ExploreProof" ] ->
   { fun ~pstate ->
-    let sigma, env = Declare.get_current_context 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/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 7779e4f4c7..d85d3bd744 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -41,6 +41,6 @@ let start_deriving f suchthat name : Declare.Proof.t =
   in
 
   let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
-  let lemma = Declare.start_dependent_proof ~name ~poly ~info goals in
+  let lemma = Declare.Proof.start_dependent ~name ~poly ~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/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 39c6c4ea54..af43c0517e 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -730,7 +730,7 @@ let extract_and_compile l =
 let show_extraction ~pstate =
   init ~inner:true false false;
   let prf = Declare.Proof.get pstate in
-  let sigma, env = Declare.get_current_context 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
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 2c85ae079f..79f311e282 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -855,13 +855,14 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
      constructing the lemma Ensures by: obvious i*)
   let info = Declare.Info.make () in
   let lemma =
-    Declare.start_proof ~name:(mk_equation_id f_id) ~poly:false ~info
+    Declare.Proof.start ~name:(mk_equation_id f_id) ~poly:false ~info
       ~impargs:[] evd lemma_type
   in
-  let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in
+  let lemma, _ =
+    Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
+  in
   let () =
-    Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent
-      ~idopt:None
+    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 a914cef6e4..50ce783579 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1520,15 +1520,15 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let typ, _ = lemmas_types_infos.(i) in
           let info = Declare.Info.make () in
           let lemma =
-            Declare.start_proof ~name:lem_id ~poly:false ~info ~impargs:[] !evd
+            Declare.Proof.start ~name:lem_id ~poly:false ~info ~impargs:[] !evd
               typ
           in
           let lemma =
-            fst @@ Declare.by (Proofview.V82.tactic (proving_tac i)) lemma
+            fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
           let () =
-            Declare.save_lemma_proved ~proof:lemma
-              ~opaque:Vernacexpr.Transparent ~idopt:None
+            Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
+              ~idopt:None
           in
           let finfo =
             match find_Function_infos (fst f_as_constant) with
@@ -1586,12 +1586,12 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let lem_id = mk_complete_id f_id in
           let info = Declare.Info.make () in
           let lemma =
-            Declare.start_proof ~name:lem_id ~poly:false sigma ~info ~impargs:[]
+            Declare.Proof.start ~name:lem_id ~poly:false sigma ~info ~impargs:[]
               (fst lemmas_types_infos.(i))
           in
           let lemma =
             fst
-              (Declare.by
+              (Declare.Proof.by
                  (Proofview.V82.tactic
                     (observe_tac
                        ("prove completeness (" ^ Id.to_string f_id ^ ")")
@@ -1599,8 +1599,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
                  lemma)
           in
           let () =
-            Declare.save_lemma_proved ~proof:lemma
-              ~opaque:Vernacexpr.Transparent ~idopt:None
+            Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
+              ~idopt:None
           in
           let finfo =
             match find_Function_infos (fst f_as_constant) with
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9f36eada45..5a188ca82b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -58,8 +58,7 @@ let declare_fun name kind ?univs value =
     (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce))
 
 let defined lemma =
-  Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent
-    ~idopt:None
+  Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
 
 let def_of_const t =
   match Constr.kind t with
@@ -1490,19 +1489,19 @@ 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
-    Declare.save_lemma_proved ~proof:lemma ~opaque:opacity ~idopt:None
+    Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
   in
   let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in
   let lemma =
-    Declare.start_proof ~name:na ~poly:false (* FIXME *) ~info ~impargs:[] sigma
+    Declare.Proof.start ~name:na ~poly:false (* FIXME *) ~info ~impargs:[] sigma
       gls_type
   in
   let lemma =
     if Indfun_common.is_strict_tcc () then
-      fst @@ Declare.by (Proofview.V82.tactic tclIDTAC) lemma
+      fst @@ Declare.Proof.by (Proofview.V82.tactic tclIDTAC) lemma
     else
       fst
-      @@ Declare.by
+      @@ Declare.Proof.by
            (Proofview.V82.tactic (fun g ->
                 tclTHEN decompose_and_tac
                   (tclORELSE
@@ -1533,18 +1532,18 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
   let start_proof env ctx tac_start tac_end =
     let info = Declare.Info.make ~hook () in
     let lemma =
-      Declare.start_proof ~name:thm_name ~poly:false (*FIXME*) ~info ctx
+      Declare.Proof.start ~name:thm_name ~poly:false (*FIXME*) ~info ctx
         ~impargs:[]
         (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
     in
     let lemma =
       fst
-      @@ Declare.by
+      @@ Declare.Proof.by
            (New.observe_tac (fun _ _ -> str "starting_tac") tac_start)
            lemma
     in
     fst
-    @@ Declare.by
+    @@ Declare.Proof.by
          (Proofview.V82.tactic
             (observe_tac
                (fun _ _ -> str "whole_start")
@@ -1607,12 +1606,12 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   let equation_lemma_type = subst1 f_constr equation_lemma_type in
   let info = Declare.Info.make () in
   let lemma =
-    Declare.start_proof ~name:eq_name ~poly:false evd ~info ~impargs:[]
+    Declare.Proof.start ~name:eq_name ~poly:false evd ~info ~impargs:[]
       (EConstr.of_constr equation_lemma_type)
   in
   let lemma =
     fst
-    @@ Declare.by
+    @@ Declare.Proof.by
          (Proofview.V82.tactic
             (start_equation f_ref terminate_ref (fun x ->
                  prove_eq
@@ -1646,8 +1645,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   in
   let _ =
     Flags.silently
-      (fun () ->
-        Declare.save_lemma_proved ~proof:lemma ~opaque:opacity ~idopt:None)
+      (fun () -> Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None)
       ()
   in
   ()
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 0c1c763b64..405fe7b844 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2000,8 +2000,8 @@ let add_morphism_interactive atts m n : Declare.Proof.t =
   let info = Declare.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->
-       let lemma = Declare.start_proof ~name:instance_id ~poly ~info ~impargs:[] evd morph in
-       fst (Declare.by (Tacinterp.interp tac) lemma)) ()
+       let lemma = Declare.Proof.start ~name:instance_id ~poly ~info ~impargs:[] evd morph in
+       fst (Declare.Proof.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
   init_setoid ();
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 1397746dd9..c8208cd444 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -363,7 +363,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
   (* 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 = Declare.start_proof ~name:id ~poly ~info ~impargs sigma termtype in
+  let lemma = Declare.Proof.start ~name:id ~poly ~info ~impargs sigma termtype in
   (* spiwack: I don't know what to do with the status here. *)
   let lemma =
     match term with
@@ -375,15 +375,15 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
           Tactics.New.reduce_after_refine;
         ]
       in
-      let lemma, _ = Declare.by init_refine lemma in
+      let lemma, _ = Declare.Proof.by init_refine lemma in
       lemma
     | None ->
-      let lemma, _ = Declare.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, _ = Declare.by tac lemma in
+    let lemma, _ = Declare.Proof.by tac lemma in
     lemma
   | None ->
     lemma
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 925a2d8389..99db8df803 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -271,7 +271,7 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   let init_terms = Some fixdefs in
   let evd = Evd.from_ctx ctx in
   let lemma =
-    Declare.start_proof_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl
+    Declare.Proof.start_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl
       evd (Some(cofix,indexes,init_terms)) thms None in
   (* Declare notations *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 29f2713192..e72f5a0397 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -2079,6 +2079,12 @@ let save_lemma_proved_delayed ~proof ~info ~idopt =
 
 module Proof = struct
   type nonrec t = t
+  let start = start_proof
+  let start_dependent = start_dependent_proof
+  let start_with_initialization = start_proof_with_initialization
+  let save = save_lemma_proved
+  let save_admitted = save_lemma_admitted
+  let by = by
   let get = get_proof
   let get_name = get_proof_name
   let fold ~f = fold_proof f
@@ -2091,4 +2097,7 @@ module Proof = struct
   let update_global_env = update_global_env
   let get_open_goals = get_open_goals
   let info { info } = info
+  let get_goal_context = get_goal_context
+  let get_current_goal_context = get_current_goal_context
+  let get_current_context = get_current_context
 end
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 25a4d80f49..10d5501285 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -133,8 +133,57 @@ module Proof : sig
 
   type t
 
-  (** XXX: These are internal and will go away from publis API once
-     lemmas is merged here *)
+  (** [start ~name ~poly ~info 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). *)
+  val start
+    :  name:Names.Id.t
+    -> poly:bool
+    -> ?impargs:Impargs.manual_implicits
+    -> info:Info.t
+    -> Evd.evar_map
+    -> EConstr.t
+    -> t
+
+  (** Like [start] except that there may be dependencies between initial goals. *)
+  val start_dependent
+    :  name:Names.Id.t
+    -> poly:bool
+    -> info:Info.t
+    -> Proofview.telescope
+    -> t
+
+  (** Pretty much internal, used by the Lemma / Fixpoint vernaculars *)
+  val start_with_initialization
+    :  ?hook:Hook.t
+    -> poly:bool
+    -> scope:Locality.locality
+    -> kind:Decls.logical_kind
+    -> udecl:UState.universe_decl
+    -> Evd.evar_map
+    -> (bool * lemma_possible_guards * Constr.t option list option) option
+    -> Recthm.t list
+    -> int list option
+    -> t
+
+  (** Qed a proof  *)
+  val save
+    : proof:t
+    -> opaque:Vernacexpr.opacity_flag
+    -> idopt:Names.lident option
+    -> unit
+
+  (** Admit a proof *)
+  val save_admitted : proof:t -> unit
+
+  (** [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
 
@@ -148,8 +197,7 @@ module Proof : sig
 
   (** 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
 
@@ -160,46 +208,27 @@ module Proof : sig
 
   val get_open_goals : t -> int
 
-  (* Internal, don't use *)
-  val info : t -> Info.t
-end
+  (** Helpers to obtain proof state when in an interactive proof *)
 
-(** [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
-  -> poly:bool
-  -> ?impargs:Impargs.manual_implicits
-  -> info:Info.t
-  -> Evd.evar_map
-  -> EConstr.t
-  -> Proof.t
+  (** [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 *)
 
-(** Like [start_proof] except that there may be dependencies between
-    initial goals. *)
-val start_dependent_proof
-  :  name:Names.Id.t
-  -> poly:bool
-  -> info:Info.t
-  -> Proofview.telescope
-  -> Proof.t
+  val get_goal_context : t -> int -> Evd.evar_map * Environ.env
 
-(** Pretty much internal, used by the Lemma / Fixpoint vernaculars *)
-val start_proof_with_initialization
-  :  ?hook:Hook.t
-  -> poly:bool
-  -> scope:Locality.locality
-  -> kind:Decls.logical_kind
-  -> udecl:UState.universe_decl
-  -> Evd.evar_map
-  -> (bool * lemma_possible_guards * Constr.t option list option) option
-  -> Recthm.t list
-  -> int list option
-  -> 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 *)
+  val info : t -> Info.t
+end
 
 (** Proof entries represent a proof that has been finished, but still
    not registered with the kernel.
@@ -300,11 +329,6 @@ val return_proof : Proof.t -> closed_proof_output
 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
@@ -315,24 +339,6 @@ 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
-
-(** [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
-
 (** Information for a constant *)
 module CInfo : sig
 
@@ -524,16 +530,6 @@ val dependencies : Obligation.t array -> int -> Int.Set.t
 
 end
 
-val save_lemma_proved
-  : proof:Proof.t
-  -> opaque:Vernacexpr.opacity_flag
-  -> idopt:Names.lident option
-  -> unit
-
-val save_lemma_admitted :
-     proof:Proof.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 :
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 86cad967b9..57aa79d749 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -146,8 +146,8 @@ let rec solve_obligation prg num tac =
   in
   let info = Declare.Info.make ~proof_ending ~scope ~kind () in
   let poly = Internal.get_poly prg in
-  let lemma = Declare.start_proof ~name:obl.obl_name ~poly ~impargs:[] ~info evd (EConstr.of_constr obl.obl_type) in
-  let lemma = fst @@ Declare.by !default_tactic lemma in
+  let lemma = Declare.Proof.start ~name:obl.obl_name ~poly ~impargs:[] ~info evd (EConstr.of_constr obl.obl_type) in
+  let lemma = fst @@ Declare.Proof.by !default_tactic lemma in
   let lemma = Option.cata (fun tac -> Declare.Proof.set_endline_tactic tac lemma) lemma tac in
   lemma
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6295587844..89294fee8c 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
@@ -95,7 +95,7 @@ let show_proof ~pstate =
   try
     let pstate = Option.get pstate in
     let p = Declare.Proof.get pstate in
-    let sigma, _ = Declare.get_current_context 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, ,
@@ -521,7 +521,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
     else (* We fix the variables to ensure they won't be lowered to Set *)
       Evd.fix_undefined_variables evd
   in
-  Declare.start_proof_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
+  Declare.Proof.start_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
 
 let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
 | Coercion ->
@@ -595,15 +595,15 @@ let vernac_start_proof ~atts kind l =
 
 let vernac_end_proof ~lemma = let open Vernacexpr in function
   | Admitted ->
-    Declare.save_lemma_admitted ~proof:lemma
+    Declare.Proof.save_admitted ~proof:lemma
   | Proved (opaque,idopt) ->
-    Declare.save_lemma_proved ~proof:lemma ~opaque ~idopt
+    Declare.Proof.save ~proof:lemma ~opaque ~idopt
 
 let vernac_exact_proof ~lemma c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the beginning of a proof. *)
-  let lemma, status = Declare.by (Tactics.exact_proof c) lemma in
-  let () = Declare.save_lemma_proved ~proof:lemma ~opaque:Opaque ~idopt:None in
+  let lemma, status = Declare.Proof.by (Tactics.exact_proof c) lemma in
+  let () = 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 =
@@ -1602,8 +1602,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
@@ -1703,7 +1703,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 *)
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 536f413bf4..2a5762b712 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -169,7 +169,7 @@ module Declare = struct
   let discard_all () = s_lemmas := None
   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