diff options
| -rw-r--r-- | test-suite/bugs/closed/3330.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v index 0bd3033acb..15303cca45 100644 --- a/test-suite/bugs/closed/3330.v +++ b/test-suite/bugs/closed/3330.v @@ -1103,3 +1103,8 @@ cannot be applied to the terms The 5th term has type "Functor (C ^op * D) set_cat" which should be coercible to "object (C ^op * D -> set_cat)". *) +End Core. + +End HoTT. + +End HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Composition_DOT_Core. |