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

2 files changed, 3 insertions, 3 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_104.v b/test-suite/bugs/closed/HoTT_coq_104.v
index ff2da3948e..5bb7fa8c12 100644
--- a/test-suite/bugs/opened/HoTT_coq_104.v
+++ b/test-suite/bugs/closed/HoTT_coq_104.v
@@ -10,4 +10,4 @@ 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).
+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/closed/HoTT_coq_124.v
index 2854c3ee4f..e6e90ada81 100644
--- a/test-suite/bugs/opened/HoTT_coq_124.v
+++ b/test-suite/bugs/closed/HoTT_coq_124.v
@@ -9,7 +9,7 @@ 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:
+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
@@ -18,7 +18,7 @@ has type
 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:
+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