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/funind/indfun.ml  | 2 +-
 plugins/funind/indfun.mli | 2 +-
 plugins/funind/recdef.ml  | 2 +-
 plugins/funind/recdef.mli | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 16df34e214..7c6669d0fc 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -634,7 +634,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
   
 
 let do_generate_principle pconstants on_error register_built interactive_proof
-    (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.pstate option =
+    (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option =
   List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl;
   let pstate, _is_struct =
     match fixpoint_exprl with
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index cd39266378..47d37b29a5 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -8,7 +8,7 @@ val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 val do_generate_principle :
   bool ->
   (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
-  Proof_global.pstate option
+  Proof_global.t option
 
 val functional_induction :
   bool ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b4d0f092d8..5a682e7231 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1495,7 +1495,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
 
 
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
-    generate_induction_principle using_lemmas : Proof_global.pstate option =
+    generate_induction_principle using_lemmas : Proof_global.t option =
   let open Term in
   let open Constr in
   let open CVars in
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 84d7a399e1..90f9c449b1 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -14,4 +14,4 @@ bool ->
            int -> Constrexpr.constr_expr -> (pconstant ->
             Indfun_common.tcc_lemma_value ref ->
             pconstant ->
-            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.pstate option
+            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option
-- 
cgit v1.2.3