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

6 files changed, 14 insertions, 14 deletions

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