From 7d7784230d91f67bdc5a3bf06caab296c64034a8 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 17 May 2014 21:42:47 -0400
Subject: A bug has been closed (HoTT/coq #105)

---
 test-suite/bugs/closed/HoTT_coq_105.v | 32 ++++++++++++++++++++++++++++++++
 test-suite/bugs/opened/HoTT_coq_105.v | 32 --------------------------------
 2 files changed, 32 insertions(+), 32 deletions(-)
 create mode 100644 test-suite/bugs/closed/HoTT_coq_105.v
 delete mode 100644 test-suite/bugs/opened/HoTT_coq_105.v

diff --git a/test-suite/bugs/closed/HoTT_coq_105.v b/test-suite/bugs/closed/HoTT_coq_105.v
new file mode 100644
index 0000000000..86001d26eb
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_105.v
@@ -0,0 +1,32 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Set Asymmetric Patterns.
+
+Inductive sum A B := inl : A -> sum A B | inr : B -> sum A B.
+Inductive Empty :=.
+
+Record category :=
+  { ob :> Type;
+    hom : ob -> ob -> Type
+  }.
+Set Printing All.
+Definition sum_category (C D : category) : category :=
+  {|
+    ob := sum (ob C) (ob D);
+    hom x y := match x, y with
+                 | inl x, inl y => @hom _ x y (* Toplevel input, characters 177-178:
+Error:
+In environment
+C : category
+D : category
+x : sum (ob C) (ob D)
+y : sum (ob C) (ob D)
+x0 : ob C
+y0 : ob C
+The term "x0" has type "ob C" while it is expected to have type
+"ob ?6" (unable to find a well-typed instantiation for
+"?6": cannot unify"Type" and "category"). *)
+                 | inr x, inr y => @hom _ x y
+                 | _, _ => Empty
+               end |}.
diff --git a/test-suite/bugs/opened/HoTT_coq_105.v b/test-suite/bugs/opened/HoTT_coq_105.v
deleted file mode 100644
index dcef0e8866..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_105.v
+++ /dev/null
@@ -1,32 +0,0 @@
-Set Primitive Projections.
-Set Implicit Arguments.
-Set Universe Polymorphism.
-Set Asymmetric Patterns.
-
-Inductive sum A B := inl : A -> sum A B | inr : B -> sum A B.
-Inductive Empty :=.
-
-Record category :=
-  { ob :> Type;
-    hom : ob -> ob -> Type
-  }.
-Set Printing All.
-Fail Definition sum_category (C D : category) : category :=
-  {|
-    ob := sum (ob C) (ob D);
-    hom x y := match x, y with
-                 | inl x, inl y => @hom _ x y (* Toplevel input, characters 177-178:
-Error:
-In environment
-C : category
-D : category
-x : sum (ob C) (ob D)
-y : sum (ob C) (ob D)
-x0 : ob C
-y0 : ob C
-The term "x0" has type "ob C" while it is expected to have type
-"ob ?6" (unable to find a well-typed instantiation for
-"?6": cannot unify"Type" and "category"). *)
-                 | inr x, inr y => @hom _ x y
-                 | _, _ => Empty
-               end |}.
-- 
cgit v1.2.3