diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-03-25 11:26:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-03-25 12:11:50 +0100 |
| commit | c1729637d4fe32ebe0268eb338fcf4d032bb5df7 (patch) | |
| tree | ea8b21f82964e360eb941d04fd8ce06c2fccc3a8 /test-suite/success/Inductive.v | |
| parent | 1a519fc37e703b014e3bcc77de01edd82aabea5f (diff) | |
Fully fixing bug #3491 (anomaly when building _rect scheme in the
presence of let-ins and recursively non-uniform parameters).
The bug was in the List.chop of Inductiveops.get_arity which was wrong
in the presence of let-ins and recursively non-uniform parameters.
The bug #3491 showed up because, in addition to have let-ins, it was
wrongly detected as having recursively non-uniform parameters.
Also added some comments in declarations.mli.
Diffstat (limited to 'test-suite/success/Inductive.v')
| -rw-r--r-- | test-suite/success/Inductive.v | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 0a4ae6873..9661b3bfa 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -139,12 +139,6 @@ Inductive IND4 (A:Type) := CONS4 : IND4 ((fun x => A) IND4) -> IND4 A. Inductive IND5 (A : Type) (T := A) : Type := CONS5 : IND5 ((fun _ => A) 0) -> IND5 A. -(* This type was raising an anomaly when building the _rect scheme, - because of a wrong computation of the number of non-recursively - uniform parameters in the presence of let-ins (see #3491) *) - -Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A. - (* An example of nested positivity which was rejected by the kernel before 24 March 2015 (even with Unset Elimination Schemes to avoid the _rect bug) due to the wrong computation of non-recursively @@ -155,3 +149,16 @@ Inductive list' (A:Type) (B:=A) := | cons' : A -> list' B -> list' A. Inductive tree := node : list' tree -> tree. + +(* This type was raising an anomaly when building the _rect scheme, + because of a bug in Inductiveops.get_arity in the presence of + let-ins and recursively non-uniform parameters. *) + +Inductive L (A:Type) (T:=A) : Type := C : L nat -> L A. + +(* This type was raising an anomaly when building the _rect scheme, + because of a wrong computation of the number of non-recursively + uniform parameters when conversion is needed, leading the example to + hit the Inductiveops.get_arity bug mentioned above (see #3491) *) + +Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A. |