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

1 files changed, 4 insertions, 3 deletions

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