diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-03-24 22:40:29 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-03-24 22:42:42 +0100 |
| commit | 7061f479eaf148779d216ad6779cf153076fb005 (patch) | |
| tree | 74d0509c2ed0ce494a52eaa9edbc44189a5b52e4 /test-suite/success/Inductive.v | |
| parent | 2e8e5cc85bfb7f2339fc38babd2dec0026ff5aa4 (diff) | |
Fixing wrong rel_context in checking positivity condition.
Parameters were missing in the context, apparently without negative
effects because the context was used only for whd normalization of
types, while reduction (in closure.ml) was resistant to unbound rels.
See however next commit for an indirect effect on the wrong
computation of non recursively uniform parameters producing an anomaly
when computing _rect schemas.
Diffstat (limited to 'test-suite/success/Inductive.v')
| -rw-r--r-- | test-suite/success/Inductive.v | 9 |
1 files changed, 9 insertions, 0 deletions
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). |