diff options
Diffstat (limited to 'test-suite/bugs/opened/HoTT_coq_080.v')
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_080.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_080.v b/test-suite/bugs/opened/HoTT_coq_080.v index 36f4780029..9f6949d395 100644 --- a/test-suite/bugs/opened/HoTT_coq_080.v +++ b/test-suite/bugs/opened/HoTT_coq_080.v @@ -23,7 +23,7 @@ Definition sum_category (C D : category) : category := Goal forall C D (x y : ob (sum_category C D)), Type. intros C D x y. hnf in x, y. -exact (hom x y). (* Toplevel input, characters 26-27: +Fail exact (hom x y). (* Toplevel input, characters 26-27: Error: In environment C : category |