diff options
| author | Matthieu Sozeau | 2014-06-17 16:49:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-17 17:19:04 +0200 |
| commit | bd755284f3fcdf7f2fced477b81d64d72226a38f (patch) | |
| tree | 651a902a2a171c74bf54055dd05f28ef04d0ec28 /test-suite | |
| parent | edd1ee4f881f9b8023524a823bcd15759038bc76 (diff) | |
Continue fix on argument scopes of primitive projections.
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". *) |