diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-29 18:18:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-29 19:03:38 +0100 |
| commit | f02f64a21863ce03f2da4ff04cd003051f96801f (patch) | |
| tree | 601fded539120c931b4ece1cff9d0790bdd82fea /pretyping/indrec.mli | |
| parent | f970991baef49fa5903e6b7aeb6ac62f8cfdf822 (diff) | |
Removing some goal unsafeness in inductive schemes.
Diffstat (limited to 'pretyping/indrec.mli')
| -rw-r--r-- | pretyping/indrec.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index f616c9679..81416a322 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -25,13 +25,13 @@ type dep_flag = bool (** Build a case analysis elimination scheme in some sort family *) -val build_case_analysis_scheme : env -> evar_map -> pinductive -> - dep_flag -> sorts_family -> evar_map * constr +val build_case_analysis_scheme : env -> 'r Sigma.t -> pinductive -> + dep_flag -> sorts_family -> (constr, 'r) Sigma.sigma (** Build a dependent case elimination predicate unless type is in Prop *) -val build_case_analysis_scheme_default : env -> evar_map -> pinductive -> - sorts_family -> evar_map * constr +val build_case_analysis_scheme_default : env -> 'r Sigma.t -> pinductive -> + sorts_family -> (constr, 'r) Sigma.sigma (** Builds a recursive induction scheme (Peano-induction style) in the same sort family as the inductive family; it is dependent if not in Prop *) |