From 5d3f54fbe38c2f732380140df96e7326c46b7b44 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 23 Aug 2014 18:21:26 +0200
Subject: Fix test-suite file.

---
 test-suite/bugs/closed/3330.v | 5 +++++
 1 file changed, 5 insertions(+)

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.
-- 
cgit v1.2.3