diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-23 18:21:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-23 18:21:50 +0200 |
| commit | 5d3f54fbe38c2f732380140df96e7326c46b7b44 (patch) | |
| tree | c42a0c51ce5fed6f92fbc89e6a7631648dd9c3f9 | |
| parent | 23c2320c5be06c0a8b86a68d4c764c7eb0b1e14f (diff) | |
Fix test-suite file.
| -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 0bd3033ac..15303cca4 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. |