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

2 files changed, 0 insertions, 42 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_104.v b/test-suite/bugs/opened/HoTT_coq_104.v
deleted file mode 100644
index ff2da3948e..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_104.v
+++ /dev/null
@@ -1,13 +0,0 @@
-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 }.
-
-Fail Check fun x : prod Set Set => eq_refl : x = pair (fst x) (snd x).
diff --git a/test-suite/bugs/opened/HoTT_coq_124.v b/test-suite/bugs/opened/HoTT_coq_124.v
deleted file mode 100644
index 2854c3ee4f..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_124.v
+++ /dev/null
@@ -1,29 +0,0 @@
-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 *)
-Fail 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)". *)
-Fail 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)". *)