Merge PR #6233: [proof] [api] Rename proof types in preparation for functionalization.

15 files changed, 87 insertions, 77 deletions

diff --git a/API/API.mli b/API/API.mli
index df5a9b131..e320e496c 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4800,24 +4800,26 @@ end
 
 module Proof :
 sig
-  type proof
-  type 'a focus_kind
+  type t
+  type proof = t
+  [@@ocaml.deprecated "please use [Proof.t]"]
 
-  val proof : proof ->
+  type 'a focus_kind
+  val proof : t ->
     Goal.goal list * (Goal.goal list * Goal.goal list) list *
     Goal.goal list * Goal.goal list * Evd.evar_map
 
   val run_tactic : Environ.env ->
-                   unit Proofview.tactic -> proof -> proof * (bool * Proofview_monad.Info.tree)
-  val unshelve : proof -> proof
-  val maximal_unfocus : 'a focus_kind -> proof -> proof
-  val pr_proof : proof -> Pp.t
+                   unit Proofview.tactic -> t -> t * (bool * Proofview_monad.Info.tree)
+  val unshelve : t -> t
+  val maximal_unfocus : 'a focus_kind -> t -> t
+  val pr_proof : t -> Pp.t
 
   module V82 :
   sig
-    val grab_evars : proof -> proof
+    val grab_evars : t -> t
 
-    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]"]
 
   end
@@ -4831,7 +4833,9 @@ end
 module Proof_global :
 sig
 
-  type state
+  type t
+  type state = t
+  [@@ocaml.deprecated "please use [Proof_global.t]"]
 
   type proof_mode = {
       name : string;
@@ -4862,14 +4866,14 @@ sig
     Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind ->
     Proofview.telescope -> proof_terminator -> unit
   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
   val compact_the_proof : unit -> unit
   val register_proof_mode : proof_mode -> 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 discard_all : unit -> unit
@@ -5000,7 +5004,7 @@ sig
   val by : unit Proofview.tactic -> bool
   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
   val cook_proof :
     unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind))
 
@@ -6113,9 +6117,9 @@ end
 module Vernacstate :
 sig
 
-  type t = { (* TODO: inline records in OCaml 4.03 *)
+  type t = {
     system  : States.state;        (* summary + libstack *)
-    proof   : Proof_global.state;  (* proof state *)
+    proof   : Proof_global.t;      (* proof state *)
     shallow : bool                 (* is the state trimmed down (libstack) *)
   }
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 9e8622c6e..36ca1bdcc 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -186,8 +186,8 @@ val pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t
 val pr_subgoal             : int -> evar_map -> goal list -> Pp.t
 val pr_concl               : int -> evar_map -> goal -> Pp.t
 
-val pr_open_subgoals       : proof:Proof.proof -> Pp.t
-val pr_nth_open_subgoal    : proof:Proof.proof -> int -> Pp.t
+val pr_open_subgoals       : proof:Proof.t -> Pp.t
+val pr_nth_open_subgoal    : proof:Proof.t -> int -> Pp.t
 val pr_evar                : evar_map -> (Evar.t * evar_info) -> Pp.t
 val pr_evars_int           : evar_map -> int -> evar_info Evar.Map.t -> Pp.t
 val pr_evars               : evar_map -> evar_info Evar.Map.t -> Pp.t
@@ -220,7 +220,7 @@ module ContextObjectMap : CMap.ExtS
 val pr_assumptionset :
   env -> types ContextObjectMap.t -> Pp.t
 
-val pr_goal_by_id : proof:Proof.proof -> Id.t -> Pp.t
+val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
 
 type printer_pr = {
  pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
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
 
 
 (**********************************************************)
diff --git a/stm/stm.ml b/stm/stm.ml
index ab44cc98b..8aa832da8 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -762,7 +762,7 @@ end = struct (* {{{ *)
   let fix_exn_ref = ref (fun x -> x)
 
   type proof_part =
-    Proof_global.state * Summary.frozen_bits (* only meta counters *)
+    Proof_global.t * Summary.frozen_bits (* only meta counters *)
 
   type partial_state =
     [ `Full of Vernacstate.t
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 1b1304db5..a4854b4a6 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -56,7 +56,7 @@ val standard_proof_terminator :
 (** {6 ... } *)
 
 (** A hook the next three functions pass to cook_proof *)
-val set_save_hook : (Proof.proof -> unit) -> unit
+val set_save_hook : (Proof.t -> unit) -> unit
 
 val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 63f358a9d..f8ec05fdb 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -484,7 +484,7 @@ let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def =
           start_proof_and_print (local, atts.polymorphic, DefinitionBody kind)
 	    [Some (lid,pl), (bl,t)] hook
     | DefineBody (bl,red_option,c,typ_opt) ->
- 	let red_option = match red_option with
+      let red_option = match red_option with
           | None -> None
           | Some r ->
             let sigma, env = Pfedit.get_current_context () in
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index eb1359d52..4a1ae14e3 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -8,7 +8,7 @@
 
 type t = {
   system  : States.state;        (* summary + libstack *)
-  proof   : Proof_global.state;  (* proof state *)
+  proof   : Proof_global.t;      (* proof state *)
   shallow : bool                 (* is the state trimmed down (libstack) *)
 }
 
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index bcfa49aa3..3ed27ddb7 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -8,7 +8,7 @@
 
 type t = {
   system  : States.state;        (* summary + libstack *)
-  proof   : Proof_global.state;  (* proof state *)
+  proof   : Proof_global.t;      (* proof state *)
   shallow : bool                 (* is the state trimmed down (libstack) *)
 }