diff options
| author | Gaëtan Gilbert | 2019-05-20 17:11:00 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:42 +0200 |
| commit | 99154fcb97653c606d2e62e0a0521c4afddff44c (patch) | |
| tree | 4e8fed2571d370acdc486f486e847a6317d60f69 /plugins/funind | |
| parent | 1ea1e218eed9792685bd7467b63a17fb5ebdbb7e (diff) | |
Rename Proof_global.{pstate -> t}
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.mli | 2 |
4 files changed, 4 insertions, 4 deletions
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 |