[proof] [api] Rename proof types in preparation for functionalization.

In particular `Proof_global.t` will become a first class object for
the upper parts of the system in a next commit.

8 files changed, 59 insertions, 53 deletions

diff --git a/proofs/goal.mli b/proofs/goal.mli
index ad968cdfb..37dd9d3c0 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -58,7 +58,7 @@ module V82 : sig
 
   (* Principal part of the progress tactical *)
   val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
-    
+
  (* Principal part of tclNOTSAMEGOAL *)
   val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index d676a0874..2acb678d7 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -74,7 +74,7 @@ val current_proof_statement :
 
 val solve : ?with_end_tac:unit Proofview.tactic ->
       Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
-      Proof.proof -> Proof.proof*bool
+      Proof.t -> Proof.t * bool
 
 (** [by tac] applies tactic [tac] to the 1st subgoal of the current
     focused proof or raises a UserError if there is no focused proof or
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 413b5fdd7..04e707cd6 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -98,7 +98,7 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k)
 
 (* Subpart of the type of proofs. It contains the parts of the proof which
    are under control of the undo mechanism *)
-type proof = {
+type t = {
   (* Current focused proofview *)
   proofview: Proofview.proofview;
   (* Entry for the proofview *)
@@ -115,6 +115,8 @@ type proof = {
   initial_euctx : UState.t
 }
 
+type proof = t
+
 (*** General proof functions ***)
 
 let proof p =
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 83777fc96..0b5e771ef 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -30,7 +30,9 @@
 *)
 
 (* Type of a proof. *)
-type proof
+type t
+type proof = t
+[@@ocaml.deprecated "please use [Proof.t]"]
 
 (* Returns a stylised view of a proof for use by, for instance,
    ide-s. *)
@@ -42,7 +44,7 @@ type proof
    shelf (the list of goals on the shelf), a representation of the
    given up goals (the list of the given up goals) and the underlying
    evar_map *)
-val proof : proof ->
+val proof : t ->
   Goal.goal list
   * (Goal.goal list * Goal.goal list) list
   * Goal.goal list
@@ -61,26 +63,26 @@ type 'a pre_goals = {
   (** List of the goals that have been given up *)
 }
 
-val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals)
+val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals)
 
 
 (*** General proof functions ***)
-val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof
-val dependent_start : Proofview.telescope -> proof
-val initial_goals : proof -> (EConstr.constr * EConstr.types) list
-val initial_euctx : proof -> UState.t
+val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> t
+val dependent_start : Proofview.telescope -> t
+val initial_goals : t -> (EConstr.constr * EConstr.types) list
+val initial_euctx : t -> UState.t
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
     to be considered (this does not require that all evars have been solved). *)
-val is_done : proof -> bool
+val is_done : t -> bool
 
 (* Like is_done, but this time it really means done (i.e. nothing left to do) *)
-val is_complete : proof -> bool
+val is_complete : t -> bool
 
 (* Returns the list of partial proofs to initial goals. *)
-val partial_proof : proof -> EConstr.constr list
+val partial_proof : t -> EConstr.constr list
 
-val compact : proof -> proof
+val compact : t -> t
 
 (* Returns the proofs (with their type) of the initial goals.
     Raises [UnfinishedProof] is some goals remain to be considered.
@@ -91,7 +93,7 @@ exception UnfinishedProof
 exception HasShelvedGoals
 exception HasGivenUpGoals
 exception HasUnresolvedEvar
-val return : proof -> Evd.evar_map
+val return : t -> Evd.evar_map
 
 (*** Focusing actions ***)
 
@@ -131,7 +133,7 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
 (* focus command (focuses on the [i]th subgoal) *)
 (* spiwack: there could also, easily be a focus-on-a-range tactic, is there 
    a need for it? *)
-val focus : 'a focus_condition -> 'a -> int -> proof -> proof
+val focus : 'a focus_condition -> 'a -> int -> t -> t
 
 exception FullyUnfocused
 exception CannotUnfocusThisWay
@@ -147,59 +149,59 @@ exception NoSuchGoals of int * int
    Raises [FullyUnfocused] if the proof is not focused.
    Raises [CannotUnfocusThisWay] if the proof the unfocusing condition
      is not met. *)
-val unfocus : 'a focus_kind -> proof -> unit -> proof
+val unfocus : 'a focus_kind -> t -> unit -> t
 
 (* [unfocused p] returns [true] when [p] is fully unfocused. *)
-val unfocused : proof -> bool
+val unfocused : t -> bool
 
 (* [get_at_focus k] gets the information stored at the closest focus point
     of kind [k].
     Raises [NoSuchFocus] if there is no focus point of kind [k]. *)
 exception NoSuchFocus
-val get_at_focus : 'a focus_kind -> proof -> 'a
+val get_at_focus : 'a focus_kind -> t -> 'a
 
 (* [is_last_focus k] check if the most recent focus is of kind [k] *)
-val is_last_focus : 'a focus_kind -> proof -> bool
+val is_last_focus : 'a focus_kind -> t -> bool
 
 (* returns [true] if there is no goal under focus. *)
-val no_focused_goal : proof -> bool
+val no_focused_goal : t -> bool
 
 (*** Tactics ***)
 
 (* the returned boolean signal whether an unsafe tactic has been
    used. In which case it is [false]. *)
 val run_tactic : Environ.env ->
-  unit Proofview.tactic -> proof -> proof*(bool*Proofview_monad.Info.tree)
+  unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree)
 
-val maximal_unfocus : 'a focus_kind -> proof -> proof
+val maximal_unfocus : 'a focus_kind -> t -> t
 
 (*** Commands ***)
 
-val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a
+val in_proof : t -> (Evd.evar_map -> 'a) -> 'a
 
 (* Remove all the goals from the shelf and adds them at the end of the
    focused goals. *)
-val unshelve : proof -> proof
+val unshelve : t -> t
 
-val pr_proof : proof -> Pp.t
+val pr_proof : t -> Pp.t
 
 (*** Compatibility layer with <=v8.2 ***)
 module V82 : sig
-  val subgoals : proof -> Goal.goal list Evd.sigma
+  val subgoals : t -> Goal.goal list Evd.sigma
   [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"]
 
   (* All the subgoals of the proof, including those which are not focused. *)
-  val background_subgoals : proof -> Goal.goal list Evd.sigma
+  val background_subgoals : t -> Goal.goal list Evd.sigma
 
-  val top_goal : proof -> Goal.goal Evd.sigma
+  val top_goal : t -> Goal.goal Evd.sigma
 
   (* returns the existential variable used to start the proof *)
-  val top_evars : proof -> Evar.t list
+  val top_evars : t -> Evar.t list
 
   (* Turns the unresolved evars into goals.
      Raises [UnfinishedProof] if there are still unsolved goals. *)
-  val grab_evars : proof -> proof
+  val grab_evars : t -> t
 
   (* Implements the Existential command *)
-  val instantiate_evar : int -> Constrexpr.constr_expr -> proof -> proof
+  val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t
 end
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index 4f575ab4b..214916331 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -25,8 +25,8 @@ let pr_bullet b =
 
 type behavior = {
   name : string;
-  put : proof -> t -> proof;
-  suggest: proof -> Pp.t
+  put : Proof.t -> t -> Proof.t;
+  suggest: Proof.t -> Pp.t
 }
 
 let behaviors = Hashtbl.create 4
@@ -110,7 +110,7 @@ module Strict = struct
   let push (b:t) pr =
     focus bullet_cond (b::get_bullets pr) 1 pr
 
-  let suggest_bullet (prf : proof): suggestion =
+  let suggest_bullet (prf : Proof.t): suggestion =
     if is_done prf then ProofFinished
     else if not (no_focused_goal prf)
     then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *)
@@ -137,7 +137,7 @@ module Strict = struct
       in
       loop prf
 
-  let rec pop_until (prf : proof) bul : proof =
+  let rec pop_until (prf : Proof.t) bul : Proof.t =
     let prf', b = pop prf in
     if bullet_eq bul b then prf'
     else pop_until prf' bul
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index 9e924fec9..09fcabf50 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -12,8 +12,6 @@
 (*                                                        *)
 (**********************************************************)
 
-open Proof
-
 type t = Vernacexpr.bullet
 
 (** A [behavior] is the data of a put function which
@@ -22,8 +20,8 @@ type t = Vernacexpr.bullet
     with a name to identify the behavior. *)
 type behavior = {
   name : string;
-  put : proof -> t -> proof;
-  suggest: proof -> Pp.t
+  put : Proof.t -> t -> Proof.t;
+  suggest: Proof.t -> Pp.t
 }
 
 (** A registered behavior can then be accessed in Coq
@@ -39,8 +37,8 @@ val register_behavior : behavior -> unit
 
 (** Handles focusing/defocusing with bullets:
      *)
-val put : proof -> t -> proof
-val suggest : proof -> Pp.t
+val put : Proof.t -> t -> Proof.t
+val suggest : Proof.t -> Pp.t
 
 (**********************************************************)
 (*                                                        *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index aa5621770..c1e1c2eda 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -90,12 +90,15 @@ type pstate = {
   terminator : proof_terminator CEphemeron.key;
   endline_tactic : Genarg.glob_generic_argument option;
   section_vars : Context.Named.t option;
-  proof : Proof.proof;
+  proof : Proof.t;
   strength : Decl_kinds.goal_kind;
   mode : proof_mode CEphemeron.key;
   universe_decl: Univdecls.universe_decl;
 }
 
+type t = pstate list
+type state = t
+
 let make_terminator f = f
 let apply_terminator f = f
 
@@ -467,8 +470,6 @@ module V82 = struct
     pid, (goals, strength)
 end
 
-type state = pstate list
-        
 let freeze ~marshallable =
   match marshallable with
   | `Yes ->
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index eed62f912..059459042 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -10,6 +10,10 @@
      toplevel. In particular it defines the global proof
      environment. *)
 
+type t
+type state = t
+[@@ocaml.deprecated "please use [Proof_global.t]"]
+
 val there_are_pending_proofs : unit -> bool
 val check_no_pending_proof : unit -> unit
 
@@ -21,7 +25,7 @@ val discard_current : unit -> unit
 val discard_all : unit -> unit
 
 exception NoCurrentProof
-val give_me_the_proof : unit -> Proof.proof
+val give_me_the_proof : unit -> Proof.t
 (** @raise NoCurrentProof when outside proof mode. *)
 
 val compact_the_proof : unit -> unit
@@ -107,9 +111,9 @@ val get_open_goals : unit -> int
     no current proof.
     The return boolean is set to [false] if an unsafe tactic has been used. *)
 val with_current_proof :
-  (unit Proofview.tactic -> Proof.proof -> Proof.proof*'a) -> 'a
+  (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
 val simple_with_current_proof :
-  (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit
+  (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit
 
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
 val set_endline_tactic : Genarg.glob_generic_argument -> unit
@@ -129,11 +133,10 @@ module V82 : sig
   Decl_kinds.goal_kind)
 end
 
-type state
-val freeze : marshallable:[`Yes | `No | `Shallow] -> state
-val unfreeze : state -> unit
-val proof_of_state : state -> Proof.proof
-val copy_terminators : src:state -> tgt:state -> state
+val freeze : marshallable:[`Yes | `No | `Shallow] -> t
+val unfreeze : t -> unit
+val proof_of_state : t -> Proof.t
+val copy_terminators : src:t -> tgt:t -> t
 
 
 (**********************************************************)