diff options
Diffstat (limited to 'test-suite/bugs/opened/HoTT_coq_124.v')
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_124.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_124.v b/test-suite/bugs/opened/HoTT_coq_124.v index e6e90ada81..2854c3ee4f 100644 --- a/test-suite/bugs/opened/HoTT_coq_124.v +++ b/test-suite/bugs/opened/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 *) -Check eqm_refl _ : eqm (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error: +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 @@ -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)". *) -Check eqp_refl _ : eqp (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error: +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 |