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

9 files changed, 50 insertions, 50 deletions

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