[declare] Rename `Declare.t` to `Declare.Proof.t`

This still needs API cleanup but we defer it to the moment we are
ready to make the internals private.

24 files changed, 131 insertions, 109 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 9ded2edcb8..8c2090f3be 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -287,7 +287,7 @@ VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
 | ![ proof_query ] [ "ExploreProof" ] ->
   { fun ~pstate ->
     let sigma, env = Declare.get_current_context pstate in
-    let pprf = Proof.partial_proof (Declare.get_proof pstate) in
+    let pprf = Proof.partial_proof (Declare.Proof.get_proof pstate) in
     Feedback.msg_notice
       (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
   }
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 3eb5057b85..f09b35a6d1 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -42,6 +42,6 @@ let start_deriving f suchthat name : Lemmas.t =
 
   let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) ~kind () in
   let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in
-  Lemmas.pf_map (Declare.map_proof begin fun p ->
+  Lemmas.pf_map (Declare.Proof.map_proof begin fun p ->
     Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
   end) lemma
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7f8e8b36ad..02383799a9 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -728,13 +728,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.get_proof pstate in
+  let prf = Declare.Proof.get_proof pstate in
   let sigma, env = Declare.get_current_context pstate in
   let trms = Proof.partial_proof prf in
   let extr_term t =
     let ast, ty = extract_constr env sigma t in
     let mp = Lib.current_mp () in
-    let l = Label.of_id (Declare.get_proof_name pstate) in
+    let l = Label.of_id (Declare.Proof.get_proof_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/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 2e1509c5cc..06cc475200 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -40,4 +40,4 @@ val structure_for_compute :
 
 (* Show the extraction of the current ongoing proof *)
 
-val show_extraction : pstate:Declare.t -> unit
+val show_extraction : pstate:Declare.Proof.t -> unit
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 51d3286715..ffb9a7e69b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -27,7 +27,6 @@ open Tacticals
 open Tacmach
 open Tactics
 open Nametab
-open Declare
 open Tacred
 open Glob_term
 open Pretyping
@@ -54,8 +53,9 @@ let find_reference sl s =
   locate (make_qualid dp (Id.of_string s))
 
 let declare_fun name kind ?univs value =
-  let ce = definition_entry ?univs value (*FIXME *) in
-  GlobRef.ConstRef (declare_constant ~name ~kind (DefinitionEntry ce))
+  let ce = Declare.definition_entry ?univs value (*FIXME *) in
+  GlobRef.ConstRef
+    (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce))
 
 let defined lemma =
   Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None
@@ -1336,7 +1336,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.get_proof pstate in
+  let p = Declare.Proof.get_proof pstate in
   let Proof.{goals = sgs; sigma; _} = Proof.data p in
   (sigma, List.map (Goal.V82.abstract_type sigma) sgs)
 
@@ -1416,7 +1416,7 @@ let is_opaque_constant c =
 let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
     (gls_type, decompose_and_tac, nb_goal) =
   (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
-  let current_proof_name = Lemmas.pf_fold Declare.get_proof_name lemma in
+  let current_proof_name = Lemmas.pf_fold Declare.Proof.get_proof_name lemma in
   let name =
     match goal_name with
     | Some s -> s
@@ -1514,7 +1514,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
                   g))
            lemma
   in
-  if Lemmas.(pf_fold Declare.get_open_goals) lemma = 0 then (
+  if Lemmas.(pf_fold Declare.Proof.get_open_goals) lemma = 0 then (
     defined lemma; None )
   else Some lemma
 
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 7ed733cf57..7754fe401e 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.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
+  -> { fun ~pstate -> Declare.Proof.map_proof (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.map_proof (fun p  -> Proof.unshelve p) pstate  }
+  -> { fun ~pstate -> Declare.Proof.map_proof (fun p  -> Proof.unshelve p) pstate  }
 END
 
 (* Gives up on the goals under focus: the goals are considered solved,
@@ -1102,7 +1102,7 @@ END
 
 VERNAC COMMAND EXTEND OptimizeProof
 | ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
-  { fun ~pstate -> Declare.compact_the_proof pstate }
+  { fun ~pstate -> Declare.Proof.compact pstate }
 | [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
   { Gc.compact () }
 END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 3cc8c4934a..e713ab13b2 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -364,7 +364,7 @@ let print_info_trace =
 
 let vernac_solve ~pstate n info tcom b =
   let open Goal_select in
-  let pstate, status = Declare.map_fold_proof_endline (fun etac p ->
+  let pstate, status = Declare.Proof.map_fold_proof_endline (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/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 1c9eae48ce..2ff76e69f8 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -50,7 +50,7 @@ let is_focused_goal_simple ~doc id =
   | `Expired | `Error _ | `Valid None -> `Not
   | `Valid (Some { Vernacstate.lemmas }) ->
     Option.cata (Vernacstate.LemmaStack.with_top_pstate ~f:(fun proof ->
-        let proof = Declare.get_proof proof in
+        let proof = Declare.Proof.get_proof 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 8dcd7bbfd5..f3768e9b99 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1164,7 +1164,7 @@ 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.get_proof) vstate.Vernacstate.lemmas
+    | `Valid (Some vstate) -> Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:Declare.Proof.get_proof) vstate.Vernacstate.lemmas
     | _ -> None
 
   let undo_vernac_classifier v ~doc =
diff --git a/tactics/declare.ml b/tactics/declare.ml
index d1b5a852b1..cce43e833e 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -882,3 +882,20 @@ let get_current_goal_context pf =
 let get_current_context pf =
   let p = get_proof pf in
   Proof.get_proof_context p
+
+module Proof = struct
+  type nonrec t = t
+  let get_proof = get_proof
+  let get_proof_name = get_proof_name
+  let get_used_variables = get_used_variables
+  let get_universe_decl = get_universe_decl
+  let get_initial_euctx = get_initial_euctx
+  let map_proof = map_proof
+  let map_fold_proof = map_fold_proof
+  let map_fold_proof_endline = map_fold_proof_endline
+  let set_endline_tactic = set_endline_tactic
+  let set_used_variables = set_used_variables
+  let compact = compact_the_proof
+  let update_global_env = update_global_env
+  let get_open_goals = get_open_goals
+end
diff --git a/tactics/declare.mli b/tactics/declare.mli
index c50772eeea..25dcc84fc8 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -31,31 +31,43 @@ open Entries
 
  *)
 
-(** [Declare.t] Interactive, unsaved constant/proof. *)
-type t
+(** [Declare.Proof.t] Construction of constants using interactive proofs. *)
+module Proof : sig
 
-(* Should be moved into a proper view *)
-val get_proof : t -> Proof.t
-val get_proof_name : t -> Names.Id.t
+  type t
 
-(** XXX: These 3 are only used in lemmas  *)
-val get_used_variables : t -> Names.Id.Set.t option
-val get_universe_decl : t -> UState.universe_decl
-val get_initial_euctx : t -> UState.t
+  (** XXX: These are internal and will go away from publis API once
+     lemmas is merged here *)
+  val get_proof : t -> Proof.t
+  val get_proof_name : t -> Names.Id.t
 
-val compact_the_proof : t -> t
+  (** XXX: These 3 are only used in lemmas  *)
+  val get_used_variables : t -> Names.Id.Set.t option
+  val get_universe_decl : t -> UState.universe_decl
+  val get_initial_euctx : t -> UState.t
 
-val map_proof : (Proof.t -> Proof.t) -> t -> t
-val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a
-val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
+  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
 
-(** 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 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
+  (** 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 compact : t -> t
+
+  (** Update the proofs global environment after a side-effecting command
+      (e.g. a sublemma definition) has been run inside it. Assumes
+      there_are_pending_proofs. *)
+  val update_global_env : t -> t
+
+  val get_open_goals : t -> int
+
+end
 
 type opacity_flag = Opaque | Transparent
 
@@ -71,7 +83,7 @@ val start_proof
   -> poly:bool
   -> Evd.evar_map
   -> (Environ.env * EConstr.types) list
-  -> t
+  -> Proof.t
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
@@ -80,12 +92,7 @@ val start_dependent_proof
   -> udecl:UState.universe_decl
   -> poly:bool
   -> Proofview.telescope
-  -> t
-
-(** Update the proofs global environment after a side-effecting command
-  (e.g. a sublemma definition) has been run inside it. Assumes
-  there_are_pending_proofs. *)
-val update_global_env : t -> t
+  -> Proof.t
 
 (** Proof entries represent a proof that has been finished, but still
    not registered with the kernel.
@@ -113,7 +120,7 @@ type proof_object = private
   (** universe state *)
   }
 
-val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> t -> proof_object
+val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t -> proof_object
 
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
@@ -243,19 +250,17 @@ end
 type closed_proof_output
 
 (** Requires a complete proof. *)
-val return_proof : t -> closed_proof_output
+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 : t -> closed_proof_output
-val close_future_proof : feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> proof_object
-
-val get_open_goals : t -> int
+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 -> t -> t * bool
+val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool
 
 (** Declare abstract constant; will check no evars are possible; *)
 val declare_abstract :
@@ -285,14 +290,14 @@ val build_by_tactic
    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 : t -> int -> Evd.evar_map * Environ.env
+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 : t -> Evd.evar_map * Environ.env
+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 : t -> Evd.evar_map * Environ.env
+val get_current_context : Proof.t -> Evd.evar_map * Environ.env
diff --git a/tactics/hints.ml b/tactics/hints.ml
index a2edafb376..ffb0e030db 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1562,7 +1562,7 @@ let pr_hint_term env sigma cl =
 (* print all hints that apply to the concl of the current goal *)
 let pr_applicable_hint pf =
   let env = Global.env () in
-  let pts = Declare.get_proof pf in
+  let pts = Declare.Proof.get_proof pf in
   let Proof.{goals;sigma} = Proof.data pts in
   match goals with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 7f870964ab..eed0e37fac 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -306,7 +306,7 @@ val wrap_hint_warning_fun : env -> evar_map ->
 (** Printing  hints *)
 
 val pr_searchtable : env -> evar_map -> Pp.t
-val pr_applicable_hint : Declare.t -> Pp.t
+val pr_applicable_hint : Declare.Proof.t -> Pp.t
 val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
 val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
 val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 136ea8b7e0..28e877491e 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -795,7 +795,7 @@ let perform_eval ~pstate e =
       Goal_select.SelectAll, Proof.start ~name ~poly sigma []
     | Some pstate ->
       Goal_select.get_default_goal_selector (),
-      Declare.get_proof pstate
+      Declare.Proof.get_proof pstate
   in
   let v = match selector with
   | Goal_select.SelectNth i -> Proofview.tclFOCUS i i v
@@ -899,7 +899,7 @@ let print_ltac qid =
 (** Calling tactics *)
 
 let solve ~pstate default tac =
-  let pstate, status = Declare.map_fold_proof_endline begin fun etac p ->
+  let pstate, status = Declare.Proof.map_fold_proof_endline begin 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
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index 5fa949ba4a..fc56a54e3a 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -31,7 +31,7 @@ val register_struct
 val register_notation : ?local:bool -> sexpr list -> int option ->
   raw_tacexpr -> unit
 
-val perform_eval : pstate:Declare.t option -> raw_tacexpr -> unit
+val perform_eval : pstate:Declare.Proof.t option -> raw_tacexpr -> unit
 
 (** {5 Notations} *)
 
@@ -53,7 +53,7 @@ val print_ltac : Libnames.qualid -> unit
 (** {5 Eval loop} *)
 
 (** Evaluate a tactic expression in the current environment *)
-val call : pstate:Declare.t -> default:bool -> raw_tacexpr -> Declare.t
+val call : pstate:Declare.Proof.t -> default:bool -> raw_tacexpr -> Declare.Proof.t
 
 (** {5 Toplevel exceptions} *)
 
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index f5a7307028..b13e5bf653 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -62,14 +62,14 @@ end
 
 (* Proofs with a save constant function *)
 type t =
-  { proof : Declare.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.set_endline_tactic t)
+let set_endline_tactic t = pf_map (Declare.Proof.set_endline_tactic t)
 
 (* To be removed *)
 module Internal = struct
@@ -173,7 +173,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
     (* 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.map_proof (fun p ->
+    pf_map (Declare.Proof.map_proof (fun p ->
         pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)) lemma
 
 (************************************************************************)
@@ -275,7 +275,7 @@ let get_keep_admitted_vars =
 
 let compute_proof_using_for_admitted proof typ pproofs =
   if not (get_keep_admitted_vars ()) then None
-  else match Declare.get_used_variables proof, pproofs with
+  else match Declare.Proof.get_used_variables proof, pproofs with
     | Some _ as x, _ -> x
     | None, pproof :: _ ->
       let env = Global.env () in
@@ -291,17 +291,17 @@ let finish_admitted ~info ~uctx pe =
   ()
 
 let save_lemma_admitted ~(lemma : t) : unit =
-  let udecl = Declare.get_universe_decl lemma.proof in
-  let Proof.{ poly; entry } = Proof.data (Declare.get_proof lemma.proof) in
+  let udecl = Declare.Proof.get_universe_decl lemma.proof in
+  let Proof.{ poly; entry } = Proof.data (Declare.Proof.get_proof lemma.proof) in
   let typ = match Proofview.initial_goals entry with
     | [typ] -> snd typ
     | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.")
   in
   let typ = EConstr.Unsafe.to_constr typ in
-  let proof = Declare.get_proof lemma.proof in
+  let proof = Declare.Proof.get_proof lemma.proof in
   let pproofs = Proof.partial_proof proof in
   let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in
-  let uctx = Declare.get_initial_euctx lemma.proof in
+  let uctx = Declare.Proof.get_initial_euctx lemma.proof in
   let univs = UState.check_univ_decl ~poly uctx udecl in
   finish_admitted ~info:lemma.info ~uctx (sec_vars, (typ, univs), None)
 
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index f8e9e1f529..bd2e87ac3a 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -19,10 +19,10 @@ type t
 val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
 (** [set_endline_tactic tac lemma] set ending tactic for [lemma] *)
 
-val pf_map : (Declare.t -> Declare.t) -> t -> t
+val pf_map : (Declare.Proof.t -> Declare.Proof.t) -> t -> t
 (** [pf_map f l] map the underlying proof object *)
 
-val pf_fold : (Declare.t -> 'a) -> t -> 'a
+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
diff --git a/vernac/search.mli b/vernac/search.mli
index 16fd303917..d3b8444b5f 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -38,13 +38,13 @@ val search_filter : glob_search_about_item -> filter_function
 goal and the global environment for things matching [pattern] and
 satisfying module exclude/include clauses of [modinout]. *)
 
-val search_by_head : ?pstate:Declare.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_by_head : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_rewrite : ?pstate:Declare.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_rewrite : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_pattern : ?pstate:Declare.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_pattern : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search         : ?pstate:Declare.t -> int option -> (bool * glob_search_about_item) list
+val search         : ?pstate:Declare.Proof.t -> int option -> (bool * glob_search_about_item) list
                   -> DirPath.t list * bool -> display_function -> unit
 
 type search_constraint =
@@ -65,12 +65,12 @@ type 'a coq_object = {
   coq_object_object : 'a;
 }
 
-val interface_search : ?pstate:Declare.t -> ?glnum:int -> (search_constraint * bool) list ->
+val interface_search : ?pstate:Declare.Proof.t -> ?glnum:int -> (search_constraint * bool) list ->
   constr coq_object list
 
 (** {6 Generic search function} *)
 
-val generic_search : ?pstate:Declare.t -> int option -> display_function -> unit
+val generic_search : ?pstate:Declare.Proof.t -> int option -> display_function -> unit
 (** This function iterates over all hypothesis of the goal numbered
     [glnum] (if present) and all known declarations. *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 860671aed7..044e479aeb 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -94,7 +94,7 @@ let show_proof ~pstate =
   (* spiwack: this would probably be cooler with a bit of polishing. *)
   try
     let pstate = Option.get pstate in
-    let p = Declare.get_proof pstate in
+    let p = Declare.Proof.get_proof pstate in
     let sigma, env = Declare.get_current_context pstate in
     let pprf = Proof.partial_proof p in
     Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
@@ -1167,7 +1167,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.map_proof (fun p ->
+  Declare.Proof.map_proof (fun p ->
       let intern env sigma = Constrintern.intern_constr env sigma com in
       Proof.V82.instantiate_evar (Global.env ()) n intern p) pstate
 
@@ -1175,12 +1175,12 @@ let vernac_set_end_tac ~pstate tac =
   let env = Genintern.empty_glob_sign (Global.env ()) in
   let _, tac = Genintern.generic_intern env tac in
   (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
-  Declare.set_endline_tactic tac pstate
+  Declare.Proof.set_endline_tactic tac pstate
 
-let vernac_set_used_variables ~pstate e : Declare.t =
+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.get_proof pstate)) in
+  let tys = List.map snd (initial_goals (Declare.Proof.get_proof 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
@@ -1189,7 +1189,7 @@ let vernac_set_used_variables ~pstate e : Declare.t =
       user_err ~hdr:"vernac_set_used_variables"
         (str "Unknown variable: " ++ Id.print id))
     l;
-  let _, pstate = Declare.set_used_variables pstate l in
+  let _, pstate = Declare.Proof.set_used_variables pstate l in
   pstate
 
 (*****************************)
@@ -1655,7 +1655,7 @@ let vernac_global_check c =
 
 
 let get_nth_goal ~pstate n =
-  let pf = Declare.get_proof pstate in
+  let pf = Declare.Proof.get_proof pstate in
   let Proof.{goals;sigma} = Proof.data pf in
   let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in
   gl
@@ -1893,7 +1893,7 @@ let vernac_register qid r =
 (* Proof management *)
 
 let vernac_focus ~pstate gln =
-  Declare.map_proof (fun p ->
+  Declare.Proof.map_proof (fun p ->
     match gln with
       | None -> Proof.focus focus_command_cond () 1 p
       | Some 0 ->
@@ -1904,13 +1904,13 @@ let vernac_focus ~pstate gln =
 
   (* Unfocuses one step in the focus stack. *)
 let vernac_unfocus ~pstate =
-  Declare.map_proof
+  Declare.Proof.map_proof
     (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.get_proof pstate in
+  let p = Declare.Proof.get_proof pstate in
   if Proof.unfocused p then
     str"The proof is indeed fully unfocused."
   else
@@ -1923,7 +1923,7 @@ let subproof_kind = Proof.new_focus_kind ()
 let subproof_cond = Proof.done_cond subproof_kind
 
 let vernac_subproof gln ~pstate =
-  Declare.map_proof (fun p ->
+  Declare.Proof.map_proof (fun p ->
     match gln with
     | None -> Proof.focus subproof_cond () 1 p
     | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
@@ -1933,12 +1933,12 @@ let vernac_subproof gln ~pstate =
     pstate
 
 let vernac_end_subproof ~pstate =
-  Declare.map_proof (fun p ->
+  Declare.Proof.map_proof (fun p ->
       Proof.unfocus subproof_kind p ())
     pstate
 
 let vernac_bullet (bullet : Proof_bullet.t) ~pstate =
-  Declare.map_proof (fun p ->
+  Declare.Proof.map_proof (fun p ->
     Proof_bullet.put p bullet) pstate
 
 (* Stack is needed due to show proof names, should deprecate / remove
@@ -1955,7 +1955,7 @@ let vernac_show ~pstate =
     end
   (* Show functions that require a proof state *)
   | Some pstate ->
-    let proof = Declare.get_proof pstate in
+    let proof = Declare.Proof.get_proof pstate in
     begin function
     | ShowGoal goalref ->
       begin match goalref with
@@ -1967,14 +1967,14 @@ let vernac_show ~pstate =
     | ShowUniverses -> show_universes ~proof
     (* Deprecate *)
     | ShowProofNames ->
-      Id.print (Declare.get_proof_name pstate)
+      Id.print (Declare.Proof.get_proof_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.get_proof pstate in
+  let pts = Declare.Proof.get_proof 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 03172b2700..d772f274a2 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -57,9 +57,9 @@ type typed_vernac =
   | VtNoProof of (unit -> unit)
   | VtCloseProof of (lemma:Lemmas.t -> unit)
   | VtOpenProof of (unit -> Lemmas.t)
-  | VtModifyProof of (pstate:Declare.t -> Declare.t)
-  | VtReadProofOpt of (pstate:Declare.t option -> unit)
-  | VtReadProof of (pstate:Declare.t -> unit)
+  | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t)
+  | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
+  | VtReadProof of (pstate:Declare.Proof.t -> unit)
 
 type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
 
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 62136aa38d..58c267080a 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -75,9 +75,9 @@ type typed_vernac =
   | VtNoProof of (unit -> unit)
   | VtCloseProof of (lemma:Lemmas.t -> unit)
   | VtOpenProof of (unit -> Lemmas.t)
-  | VtModifyProof of (pstate:Declare.t -> Declare.t)
-  | VtReadProofOpt of (pstate:Declare.t option -> unit)
-  | VtReadProof of (pstate:Declare.t -> unit)
+  | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t)
+  | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
+  | VtReadProof of (pstate:Declare.Proof.t -> unit)
 
 type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
 
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 14f477663d..19d41c4770 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -209,7 +209,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.update_global_env) pstack)
+       else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Declare.Proof.update_global_env) pstack)
     ~st
 
 (* XXX: This won't properly set the proof mode, as of today, it is
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index d1e0dce116..0fca1e9078 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -45,7 +45,7 @@ module LemmaStack = struct
     | Some (l,ls) -> a, (l :: ls)
 
   let get_all_proof_names (pf : t) =
-    let prj x = Lemmas.pf_fold Declare.get_proof x in
+    let prj x = Lemmas.pf_fold Declare.Proof.get_proof x in
     let (pn, pns) = map Proof.(function pf -> (data (prj pf)).name) pf in
     pn :: pns
 
@@ -145,18 +145,18 @@ module Declare = struct
     | Some x -> s_lemmas := Some (LemmaStack.map_top_pstate ~f x)
 
   let there_are_pending_proofs () = !s_lemmas <> None
-  let get_open_goals () = cc get_open_goals
+  let get_open_goals () = cc Proof.get_open_goals
 
-  let give_me_the_proof_opt () = Option.map (LemmaStack.with_top_pstate ~f:get_proof) !s_lemmas
-  let give_me_the_proof () = cc get_proof
-  let get_current_proof_name () = cc get_proof_name
+  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 map_proof f = dd (map_proof f)
+  let map_proof f = dd (Proof.map_proof f)
   let with_current_proof f =
     match !s_lemmas with
     | None -> raise NoCurrentProof
     | Some stack ->
-      let pf, res = LemmaStack.with_top_pstate stack ~f:(map_fold_proof_endline f) in
+      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
       s_lemmas := Some stack;
       res
@@ -176,7 +176,7 @@ module Declare = struct
                         Lemmas.Internal.get_info pt)
 
   let discard_all () = s_lemmas := None
-  let update_global_env () = dd (update_global_env)
+  let update_global_env () = dd (Proof.update_global_env)
 
   let get_current_context () = cc Declare.get_current_context
 
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 2cabbe35f5..fb6d8b6db6 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -25,8 +25,8 @@ module LemmaStack : sig
   val pop : t -> Lemmas.t * t option
   val push : t option -> Lemmas.t -> t
 
-  val map_top_pstate : f:(Declare.t -> Declare.t) -> t -> t
-  val with_top_pstate : t -> f:(Declare.t -> 'a ) -> 'a
+  val map_top_pstate : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t
+  val with_top_pstate : t -> f:(Declare.Proof.t -> 'a ) -> 'a
 
 end
 
@@ -89,7 +89,7 @@ module Declare : sig
   val get : unit -> LemmaStack.t option
   val set : LemmaStack.t option -> unit
 
-  val get_pstate : unit -> Declare.t option
+  val get_pstate : unit -> Declare.Proof.t option
 
   val freeze : marshallable:bool -> LemmaStack.t option
   val unfreeze : LemmaStack.t -> unit