diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-07-03 18:51:13 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-07-03 18:53:17 +0200 |
commit | e7ba2a9be24823503495e959f0dffc131e99801b (patch) | |
tree | db0a3979974c88e101804438cfb89c1ddc70742d /test-suite | |
parent | f2327aa3c69f1695f99e2ccbfe00c4e54e56e7d2 (diff) |
Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanly when called
on partially applied constructors. Also protect evar_conv from that case.
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_078.v (renamed from test-suite/bugs/opened/HoTT_coq_078.v) | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_078.v b/test-suite/bugs/closed/HoTT_coq_078.v index a2c97d067..54cb68b0a 100644 --- a/test-suite/bugs/opened/HoTT_coq_078.v +++ b/test-suite/bugs/closed/HoTT_coq_078.v @@ -35,11 +35,9 @@ Definition transport_prod' {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a') | idpath => idpath end. (* success *) -Fail Definition transport_prod {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a') +Definition transport_prod {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a') (z : P a * Q a) : transport (fun a => P a * Q a) p z = (transport _ p (fst z), transport _ p (snd z)) := match p with | idpath => idpath end. -(** Toplevel input, characters 15-255: -Error: Conversion test raised an anomaly *) |