From 83dff8025ae4cf919ea92d39e4619e72fe9b3f42 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 17 Jun 2014 17:09:21 +0200
Subject: Bug closed, now in polymorphic mode, Variables A B : Type give
 different levels to A and B.

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

diff --git a/test-suite/bugs/closed/HoTT_coq_101.v b/test-suite/bugs/closed/HoTT_coq_101.v
new file mode 100644
index 0000000000..9c89a6ab9d
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_101.v
@@ -0,0 +1,77 @@
+Set Universe Polymorphism.
+Set Implicit Arguments.
+Generalizable All Variables.
+
+Record SpecializedCategory (obj : Type) :=
+  {
+    Object :> _ := obj;
+    Morphism : obj -> obj -> Type
+  }.
+
+
+Record > Category :=
+  {
+    CObject : Type;
+
+    UnderlyingCategory :> @SpecializedCategory CObject
+  }.
+
+Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
+  {
+    ObjectOf :> objC -> objD;
+    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
+  }.
+
+(* Replacing this with [Definition Functor (C D : Category) :=
+SpecializedFunctor C D.] gets rid of the universe inconsistency. *)
+Section Functor.
+  Variable C D : Category.
+
+  Definition Functor := SpecializedFunctor C D.
+End Functor.
+
+Record SpecializedNaturalTransformation `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) (F G : SpecializedFunctor C D) :=
+  {
+    ComponentsOf :> forall c, D.(Morphism) (F c) (G c)
+  }.
+
+Definition FunctorProduct' `(F : Functor C D) : SpecializedFunctor C D.
+admit.
+Defined.
+
+Definition TypeCat : @SpecializedCategory Type.
+  admit.
+Defined.
+
+
+Definition CovariantHomFunctor `(C : @SpecializedCategory objC) : SpecializedFunctor C TypeCat.
+  refine (Build_SpecializedFunctor C TypeCat
+                                   (fun X : C => C.(Morphism) X X)
+                                   _
+         ); admit.
+Defined.
+
+Definition FunctorCategory `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) : @SpecializedCategory (SpecializedFunctor C D).
+  refine (@Build_SpecializedCategory _
+                                     (SpecializedNaturalTransformation (C := C) (D := D))).
+Defined.
+
+Definition Yoneda `(C : @SpecializedCategory objC) : SpecializedFunctor C (FunctorCategory C TypeCat).
+  match goal with
+    | [ |- SpecializedFunctor ?C0 ?D0 ] =>
+      refine (Build_SpecializedFunctor C0 D0
+                                       (fun c => CovariantHomFunctor C)
+                                       _
+             )
+  end;
+  admit.
+Defined.
+
+Section FullyFaithful.
+  Context `(C : @SpecializedCategory objC).
+  Let TypeCatC := FunctorCategory C TypeCat.
+  Let YC := (Yoneda C).
+  Set Printing Universes.
+  Check @FunctorProduct' C TypeCatC YC. (* Toplevel input, characters 0-37:
+Error: Universe inconsistency. Cannot enforce Top.187 = Top.186 because
+Top.186 <= Top.189 < Top.191 <= Top.187). *)
diff --git a/test-suite/bugs/opened/HoTT_coq_101.v b/test-suite/bugs/opened/HoTT_coq_101.v
deleted file mode 100644
index 9419c25c30..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_101.v
+++ /dev/null
@@ -1,77 +0,0 @@
-Set Universe Polymorphism.
-Set Implicit Arguments.
-Generalizable All Variables.
-
-Record SpecializedCategory (obj : Type) :=
-  {
-    Object :> _ := obj;
-    Morphism : obj -> obj -> Type
-  }.
-
-
-Record > Category :=
-  {
-    CObject : Type;
-
-    UnderlyingCategory :> @SpecializedCategory CObject
-  }.
-
-Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
-  {
-    ObjectOf :> objC -> objD;
-    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
-  }.
-
-(* Replacing this with [Definition Functor (C D : Category) :=
-SpecializedFunctor C D.] gets rid of the universe inconsistency. *)
-Section Functor.
-  Variable C D : Category.
-
-  Definition Functor := SpecializedFunctor C D.
-End Functor.
-
-Record SpecializedNaturalTransformation `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) (F G : SpecializedFunctor C D) :=
-  {
-    ComponentsOf :> forall c, D.(Morphism) (F c) (G c)
-  }.
-
-Definition FunctorProduct' `(F : Functor C D) : SpecializedFunctor C D.
-admit.
-Defined.
-
-Definition TypeCat : @SpecializedCategory Type.
-  admit.
-Defined.
-
-
-Definition CovariantHomFunctor `(C : @SpecializedCategory objC) : SpecializedFunctor C TypeCat.
-  refine (Build_SpecializedFunctor C TypeCat
-                                   (fun X : C => C.(Morphism) X X)
-                                   _
-         ); admit.
-Defined.
-
-Definition FunctorCategory `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) : @SpecializedCategory (SpecializedFunctor C D).
-  refine (@Build_SpecializedCategory _
-                                     (SpecializedNaturalTransformation (C := C) (D := D))).
-Defined.
-
-Definition Yoneda `(C : @SpecializedCategory objC) : SpecializedFunctor C (FunctorCategory C TypeCat).
-  match goal with
-    | [ |- SpecializedFunctor ?C0 ?D0 ] =>
-      refine (Build_SpecializedFunctor C0 D0
-                                       (fun c => CovariantHomFunctor C)
-                                       _
-             )
-  end;
-  admit.
-Defined.
-
-Section FullyFaithful.
-  Context `(C : @SpecializedCategory objC).
-  Let TypeCatC := FunctorCategory C TypeCat.
-  Let YC := (Yoneda C).
-  Set Printing Universes.
-  Fail Check @FunctorProduct' C TypeCatC YC. (* Toplevel input, characters 0-37:
-Error: Universe inconsistency. Cannot enforce Top.187 = Top.186 because
-Top.186 <= Top.189 < Top.191 <= Top.187). *)
-- 
cgit v1.2.3