diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-22 17:17:49 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-22 21:17:25 +0100 |
commit | af954522789043202d9c300a0bb37cbaf4958d60 (patch) | |
tree | 7c8cfb9615c82ee3a78ff7f0f2e911dac4004f24 /test-suite/success/Case22.v | |
parent | e583a79b5a0298fd08f34305cc876d5117913e95 (diff) |
Fixing a bug of adjust_subst_to_rel_context.
Diffstat (limited to 'test-suite/success/Case22.v')
-rw-r--r-- | test-suite/success/Case22.v | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v index 8c8f02ecc..f88051f8f 100644 --- a/test-suite/success/Case22.v +++ b/test-suite/success/Case22.v @@ -30,14 +30,26 @@ Check fun x:I2 nat nat => match x in I2 _ X Y Z return X*Y*Z with (* This used to succeed in 8.3, 8.4 and 8.5beta1 *) Inductive IND : forall X:Type, let Y:=X in Type := - C : IND True. + CONSTR : IND True. Definition F (x:IND True) (A:Type) := (* This failed in 8.5beta2 though it should have been accepted *) - match x in IND Y Z return Z with - C => I + match x in IND X Y return Y with + CONSTR => Logic.I end. Theorem paradox : False. (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *) Fail Proof (F C False). + +(* Another bug found in November 2015 (a substitution was wrongly + reversed at pretyping level) *) + +Inductive Ind (A:Type) : + let X:=A in forall Y:Type, let Z:=(X*Y)%type in Type := + Constr : Ind A nat. + +Check fun x:Ind bool nat => + match x in Ind _ X Y Z return Z with + | Constr _ => (true,0) + end. |