diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_085.v (renamed from test-suite/bugs/opened/HoTT_coq_085.v) | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_085.v b/test-suite/bugs/closed/HoTT_coq_085.v index 43ca6864f4..041c67997f 100644 --- a/test-suite/bugs/opened/HoTT_coq_085.v +++ b/test-suite/bugs/closed/HoTT_coq_085.v @@ -67,7 +67,7 @@ Module failure. Check ((_ o _) _2 _)%hom. (* ((?14 o ?15)%functor _1 ?18)%hom : hom ?13 (ob_of (?14 o ?15)%functor ?16) (ob_of (?14 o ?15)%functor ?17) *) - Fail Check ((_ o _) _1 _)%hom. (* Toplevel input, characters 7-19: + Check ((_ o _) _1 _)%hom. (* Toplevel input, characters 7-19: Error: The term "(?23 o ?24)%hom" has type "hom ?19 ?20 ?22" while it is expected to have type "functor ?25 ?26". *) |