diff options
| -rw-r--r-- | kernel/indtypes.ml | 9 | ||||
| -rw-r--r-- | test-suite/success/Inductive.v | 9 |
2 files changed, 13 insertions, 5 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 799471c68..49bf3281f 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -346,7 +346,7 @@ let typecheck_inductive env mie = in (id,cn,lc,(sign,arity))) inds - in (env_arities, params, inds) + in (env_arities, env_ar_par, params, inds) (************************************************************************) (************************************************************************) @@ -366,9 +366,8 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum -let explain_ind_err id ntyp env0 nbpar c nargs err = +let explain_ind_err id ntyp env nbpar c nargs err = let (lpar,c') = mind_extract_params nbpar c in - let env = push_rel_context lpar env0 in match err with | LocalNonPos kt -> raise (InductiveError (NonPos (env,c',mkRel (kt+nbpar)))) @@ -822,9 +821,9 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re let check_inductive env kn mie = (* First type-check the inductive definition *) - let (env_ar, params, inds) = typecheck_inductive env mie in + let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in (* Then check positivity conditions *) - let (nmr,recargs) = check_positivity kn env_ar params inds in + let (nmr,recargs) = check_positivity kn env_ar_par params inds in (* Build the inductive packets *) build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 3d4257543..04d92daad 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -121,3 +121,12 @@ Inductive foo1 : forall p, Prop := cc1 : foo1 0. (* Check cross inference of evars from constructors *) Inductive foo2 : forall p, Prop := cc2 : forall q, foo2 q | cc3 : foo2 0. + +(* An example with reduction removing an occurrence of the inductive type in one of its argument *) + +Inductive IND1 (A:Type) := CONS1 : IND1 ((fun x => A) IND1). + +(* This type was considered as ill-formed before March 2015, while it + could be accepted considering that the type IND1 above was accepted *) + +Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2). |