From 99154fcb97653c606d2e62e0a0521c4afddff44c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 20 May 2019 17:11:00 +0200
Subject: Rename Proof_global.{pstate -> t}

---
 user-contrib/Ltac2/tac2entries.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index 273cf02c9b..80d48f67ba 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -29,7 +29,7 @@ val register_struct
 val register_notation : ?local:bool -> sexpr list -> int option ->
   raw_tacexpr -> unit
 
-val perform_eval : pstate:Proof_global.pstate option -> raw_tacexpr -> unit
+val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit
 
 (** {5 Notations} *)
 
@@ -51,7 +51,7 @@ val print_ltac : Libnames.qualid -> unit
 (** {5 Eval loop} *)
 
 (** Evaluate a tactic expression in the current environment *)
-val call : pstate:Proof_global.pstate -> default:bool -> raw_tacexpr -> Proof_global.pstate
+val call : pstate:Proof_global.t -> default:bool -> raw_tacexpr -> Proof_global.t
 
 (** {5 Toplevel exceptions} *)
 
-- 
cgit v1.2.3