diff options
author | 2014-06-17 17:34:05 +0200 | |
---|---|---|
committer | 2014-06-17 17:34:05 +0200 | |
commit | 258cbd1d2619cc5916dd570b95050e37c06fba77 (patch) | |
tree | 7f4a5cb362b4fe4fe062f6dd542943504ad99e46 /test-suite/bugs/closed/HoTT_coq_124.v | |
parent | 35d92d68c0b2123a3994a90ef7e2b8cbb946f041 (diff) |
Reinstate eta for records in evarconv, fixing two HoTT coq bugs.
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_124.v')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_124.v | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_124.v b/test-suite/bugs/closed/HoTT_coq_124.v new file mode 100644 index 000000000..e6e90ada8 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_124.v @@ -0,0 +1,29 @@ +Set Implicit Arguments. +Set Primitive Projections. + +Polymorphic Inductive eqp A (x : A) : A -> Type := eqp_refl : eqp x x. +Monomorphic Inductive eqm A (x : A) : A -> Type := eqm_refl : eqm x x. + +Polymorphic Record prodp (A B : Type) : Type := pairp { fstp : A; sndp : B }. +Monomorphic Record prodm (A B : Type) : Type := pairm { fstm : A; sndm : B }. + +Check eqm_refl _ : eqm (fun x : prodm Set Set => pairm (fstm x) (sndm x)) (fun x => x). (* success *) +Check eqp_refl _ : eqp (fun x : prodm Set Set => pairm (fstm x) (sndm x)) (fun x => x). (* success *) +Check eqm_refl _ : eqm (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error: +The term + "eqm_refl (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})" +has type + "eqm (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |}) + (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})" +while it is expected to have type + "eqm (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |}) + (fun x : prodp Set Set => x)". *) +Check eqp_refl _ : eqp (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error: +The term + "eqp_refl (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})" +has type + "eqp (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |}) + (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})" +while it is expected to have type + "eqp (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |}) + (fun x : prodp Set Set => x)". *) |