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}

---
 plugins/ltac/rewrite.ml  | 2 +-
 plugins/ltac/rewrite.mli | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 5d57a2f27f..26d477fee0 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1973,7 +1973,7 @@ let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
       Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
 
-let add_morphism_infer atts m n : Proof_global.pstate option =
+let add_morphism_infer atts m n : Proof_global.t option =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index e1cbc46b3b..5aabb946d5 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -101,7 +101,7 @@ val add_setoid
   -> Id.t
   -> unit
 
-val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.pstate option
+val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option
 
 val add_morphism
   : rewrite_attributes
@@ -109,7 +109,7 @@ val add_morphism
   -> constr_expr
   -> constr_expr
   -> Id.t
-  -> Proof_global.pstate
+  -> Proof_global.t
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
 
-- 
cgit v1.2.3