From c7284415e4bdd3315c84c7d15d140d3fee000bc5 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 9 May 2014 10:13:32 -0400
Subject: Move opened bugs to bugs/opened

---
 test-suite/bugs/closed/HoTT_coq_020.v | 83 -----------------------------------
 1 file changed, 83 deletions(-)
 delete mode 100644 test-suite/bugs/closed/HoTT_coq_020.v

(limited to 'test-suite/bugs/closed/HoTT_coq_020.v')

diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v
deleted file mode 100644
index 6747d6af2..000000000
--- a/test-suite/bugs/closed/HoTT_coq_020.v
+++ /dev/null
@@ -1,83 +0,0 @@
-Set Implicit Arguments.
-
-Generalizable All Variables.
-
-Set Asymmetric Patterns.
-
-Polymorphic Record Category (obj : Type) :=
-  Build_Category {
-      Object :> _ := obj;
-      Morphism : obj -> obj -> Type;
-
-      Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
-    }.
-
-Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) :=
-  { ObjectOf :> objC -> objD }.
-
-Polymorphic Record NaturalTransformation objC C objD D (F G : Functor (objC := objC) C (objD := objD) D) :=
-  { ComponentsOf' :> forall c, D.(Morphism) (F.(ObjectOf) c) (G.(ObjectOf) c);
-    Commutes' : forall s d (m : C.(Morphism) s d), ComponentsOf' s = ComponentsOf' s }.
-
-Ltac present_obj from to :=
-  repeat match goal with
-           | [ _ : appcontext[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in *
-           | [ |- appcontext[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in *
-         end.
-
-Section NaturalTransformationComposition.
-  Set Universe Polymorphism.
-  Context `(C : @Category objC).
-  Context `(D : @Category objD).
-  Context `(E : @Category objE).
-  Variables F F' F'' : Functor C D.
-  Unset Universe Polymorphism.
-
-  Polymorphic Definition NTComposeT (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F') :
-    NaturalTransformation F F''.
-    exists (fun c => Compose _ _ _ _ (T' c) (T c)).
-    progress present_obj @Morphism @Morphism. (* removing this line makes the error go away *)
-    intros. (* removing this line makes the error go away *)
-    admit.
-  Defined.
-End NaturalTransformationComposition.
-
-
-Polymorphic Definition FunctorCategory objC (C : Category objC) objD (D : Category objD) :
-  @Category (Functor C D)
-  := @Build_Category (Functor C D)
-                     (NaturalTransformation (C := C) (D := D))
-                     (NTComposeT (C := C) (D := D)).
-
-Polymorphic Definition Cat0 : Category Empty_set
-  := @Build_Category Empty_set
-                     (@eq _)
-                     (fun x => match x return _ with end).
-
-Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C
-  := Build_Functor Cat0 C (fun x => match x with end).
-
-Section Law0.
-  Variable objC : Type.
-  Variable C : Category objC.
-
-  Set Printing All.
-  Set Printing Universes.
-  Set Printing Existential Instances.
-
-  Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf : Object (FunctorCategory Cat0 C).
-    hnf.
-    refine (@FunctorFrom0 _ _).
-    (* Toplevel input, characters 23-40:
-Error:
-In environment
-objC : Type (* Top.61069 *)
-C : Category (* Top.61069 Top.61071 *) objC
-The term
- "@FunctorFrom0 (* Top.61077 Top.61078 *) ?69 (* [objC, C] *)
-    ?70 (* [objC, C] *)" has type
- "@Functor (* Set Prop Top.61077 Top.61078 *) Empty_set Cat0
-    ?69 (* [objC, C] *) ?70 (* [objC, C] *)"
- while it is expected to have type
- "@Functor (* Set Prop Set Prop *) Empty_set Cat0 objC C".
-*)
-- 
cgit v1.2.3