Reinstate eta for records in evarconv, fixing two HoTT coq bugs.

2 files changed, 42 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_104.v b/test-suite/bugs/closed/HoTT_coq_104.v
new file mode 100644
index 0000000000..5bb7fa8c12
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_104.v
@@ -0,0 +1,13 @@
+Set Implicit Arguments.
+
+Require Import Logic.
+
+Global Set Universe Polymorphism.
+Global Set Asymmetric Patterns.
+Local Set Record Elimination Schemes.
+Local Set Primitive Projections.
+
+Record prod (A B : Type) : Type :=
+  pair { fst : A; snd : B }.
+
+Check fun x : prod Set Set => eq_refl : x = pair (fst x) (snd x).
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 0000000000..e6e90ada81
--- /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)". *)