- Fix xml plugin treatment of inductives.

- Move HoTT bug #30 to closed

3 files changed, 2 insertions, 266 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_027.v b/test-suite/bugs/opened/HoTT_coq_027.v
index e58092eb6f..7f283237a1 100644
--- a/test-suite/bugs/opened/HoTT_coq_027.v
+++ b/test-suite/bugs/opened/HoTT_coq_027.v
@@ -20,8 +20,8 @@ Identity Coercion FunctorToType_Id : FunctorToType >-> Functor.
 
 Set Printing Universes.
 Definition FunctorTo_Set2Type `(C : @Category objC) (F : FunctorToSet C)
-: FunctorToType C.
-  Fail refine (@Build_Functor _ C _ TypeCat
+: FunctorToType@{Type Type Type Set} C.
+  refine (@Build_Functor _ C _ TypeCat
                          (fun x => F.(ObjectOf) x)
                          (fun s d m => F.(MorphismOf) _ _ m)).
 (* ??? Toplevel input, characters 8-148:
@@ -40,7 +40,6 @@ The term
  "FunctorToType@{Top.100 Top.101 Top.102 Top.103} C"
 (Universe inconsistency: Cannot enforce Set = Top.103)).
  *)
-admit.
 Defined. (* Toplevel input, characters 0-8:
 Error:
 The term
diff --git a/test-suite/bugs/opened/HoTT_coq_030.v b/test-suite/bugs/opened/HoTT_coq_030.v
deleted file mode 100644
index 934fcd5d82..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_030.v
+++ /dev/null
@@ -1,241 +0,0 @@
-Set Implicit Arguments.
-Generalizable All Variables.
-Set Asymmetric Patterns.
-Set Universe Polymorphism.
-
-Delimit Scope object_scope with object.
-Delimit Scope morphism_scope with morphism.
-Delimit Scope category_scope with category.
-Delimit Scope functor_scope with functor.
-
-Local Open Scope category_scope.
-
-Record SpecializedCategory (obj : Type) :=
-  {
-    Object :> _ := obj;
-    Morphism : obj -> obj -> Type;
-
-    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
-  }.
-
-Bind Scope category_scope with SpecializedCategory.
-Bind Scope object_scope with Object.
-Bind Scope morphism_scope with Morphism.
-
-Arguments Object {obj%type} C%category / : rename.
-Arguments Morphism {obj%type} !C%category s d : rename. (* , simpl nomatch. *)
-Arguments Compose {obj%type} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
-
-Record Category := {
-  CObject : Type;
-
-  UnderlyingCategory :> @SpecializedCategory CObject
-}.
-
-Definition GeneralizeCategory `(C : @SpecializedCategory obj) : Category.
-  refine {| CObject := C.(Object) |}; auto. (* Changing this [auto] to [assumption] removes the universe inconsistency. *)
-Defined.
-
-Coercion GeneralizeCategory : SpecializedCategory >-> Category.
-
-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)
-    }.
-
-Section Functor.
-  Variable C D : Category.
-
-  Definition Functor := SpecializedFunctor C D.
-End Functor.
-
-Bind Scope functor_scope with SpecializedFunctor.
-Bind Scope functor_scope with Functor.
-
-Arguments SpecializedFunctor {objC} C {objD} D.
-Arguments Functor C D.
-Arguments ObjectOf {objC%type C%category objD%type D%category} F%functor c%object : rename, simpl nomatch.
-Arguments MorphismOf {objC%type} [C%category] {objD%type} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
-
-Section FunctorComposition.
-  Context `(B : @SpecializedCategory objB).
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(E : @SpecializedCategory objE).
-
-  Definition ComposeFunctors (G : SpecializedFunctor D E) (F : SpecializedFunctor C D) : SpecializedFunctor C E
-    := Build_SpecializedFunctor C E
-                                (fun c => G (F c))
-                                (fun _ _ m => G.(MorphismOf) (F.(MorphismOf) m)).
-End FunctorComposition.
-
-Record SpecializedNaturalTransformation
-       `{C : @SpecializedCategory objC}
-       `{D : @SpecializedCategory objD}
-       (F G : SpecializedFunctor C D)
-  := {
-      ComponentsOf :> forall c, D.(Morphism) (F c) (G c)
-    }.
-
-Definition ProductCategory
-           `(C : @SpecializedCategory objC)
-           `(D : @SpecializedCategory objD)
-: @SpecializedCategory (objC * objD)%type
-  := @Build_SpecializedCategory _
-                                (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type)
-                                (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1))).
-
-Infix "*" := ProductCategory : category_scope.
-
-Section ProductCategoryFunctors.
-  Context `{C : @SpecializedCategory objC}.
-  Context `{D : @SpecializedCategory objD}.
-
-  Definition fst_Functor : SpecializedFunctor (C * D) C
-    := Build_SpecializedFunctor (C * D) C
-                                (@fst _ _)
-                                (fun _ _ => @fst _ _).
-
-  Definition snd_Functor : SpecializedFunctor (C * D) D
-    := Build_SpecializedFunctor (C * D) D
-                                (@snd _ _)
-                                (fun _ _ => @snd _ _).
-End ProductCategoryFunctors.
-
-
-Definition OppositeCategory `(C : @SpecializedCategory objC) : @SpecializedCategory objC :=
-  @Build_SpecializedCategory objC
-                             (fun s d => Morphism C d s)
-                             (fun _ _ _ m1 m2 => Compose m2 m1).
-
-Section OppositeFunctor.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Variable F : SpecializedFunctor C D.
-  Let COp := OppositeCategory C.
-  Let DOp := OppositeCategory D.
-
-  Definition OppositeFunctor : SpecializedFunctor COp DOp
-    := Build_SpecializedFunctor COp DOp
-                                (fun c : COp => F c : DOp)
-                                (fun (s d : COp) (m : C.(Morphism) d s) => MorphismOf F (s := d) (d := s) m).
-End OppositeFunctor.
-
-Section FunctorProduct.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(D' : @SpecializedCategory objD').
-
-  Definition FunctorProduct (F : Functor C D) (F' : Functor C D') : SpecializedFunctor C (D * D').
-    match goal with
-      | [ |- SpecializedFunctor ?C0 ?D0 ] =>
-        refine (Build_SpecializedFunctor
-                  C0 D0
-                  (fun c => (F c, F' c))
-                  (fun s d m => (MorphismOf F m, MorphismOf F' m)))
-    end.
-  Defined.
-End FunctorProduct.
-
-Section FunctorProduct'.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Context `(C' : @SpecializedCategory objC').
-  Context `(D' : @SpecializedCategory objD').
-  Variable F : Functor C D.
-  Variable F' : Functor C' D'.
-
-  Definition FunctorProduct' : SpecializedFunctor  (C * C') (D * D')
-    := FunctorProduct (ComposeFunctors F fst_Functor) (ComposeFunctors F' snd_Functor).
-End FunctorProduct'.
-
-(** XXX TODO(jgross): Change this to [FunctorProduct]. *)
-Infix "*" := FunctorProduct' : functor_scope.
-
-Definition TypeCat : @SpecializedCategory Type :=
-  (@Build_SpecializedCategory Type
-                              (fun s d => s -> d)
-                              (fun _ _ _ f g => (fun x => f (g x)))).
-
-Section HomFunctor.
-  Context `(C : @SpecializedCategory objC).
-  Let COp := OppositeCategory C.
-
-  Definition CovariantHomFunctor (A : COp) : SpecializedFunctor C TypeCat
-    := Build_SpecializedFunctor C TypeCat
-                                (fun X : C => C.(Morphism) A X : TypeCat)
-                                (fun X Y f => (fun g : C.(Morphism) A X => Compose f g)).
-
-  Definition hom_functor_object_of (c'c : COp * C) := C.(Morphism) (fst c'c) (snd c'c) : TypeCat.
-
-  Definition hom_functor_morphism_of (s's : (COp * C)%type) (d'd : (COp * C)%type) (hf : (COp * C).(Morphism) s's d'd) :
-    TypeCat.(Morphism) (hom_functor_object_of s's) (hom_functor_object_of d'd).
-    unfold hom_functor_object_of in *.
-    destruct s's as [ s' s ], d'd as [ d' d ].
-    destruct hf as [ h f ].
-    intro g.
-    exact (Compose f (Compose g h)).
-  Defined.
-
-  Definition HomFunctor : SpecializedFunctor (COp * C) TypeCat
-    := Build_SpecializedFunctor (COp * C) TypeCat
-                                (fun c'c : COp * C => C.(Morphism) (fst c'c) (snd c'c) : TypeCat)
-                                (fun X Y (hf : (COp * C).(Morphism) X Y) => hom_functor_morphism_of hf).
-End HomFunctor.
-
-Section FullFaithful.
-  Context `(C : @SpecializedCategory objC).
-  Context `(D : @SpecializedCategory objD).
-  Variable F : SpecializedFunctor C D.
-  Let COp := OppositeCategory C.
-  Let DOp := OppositeCategory D.
-  Let FOp := OppositeFunctor F.
-
-  Definition InducedHomNaturalTransformation :
-    SpecializedNaturalTransformation (HomFunctor C) (ComposeFunctors (HomFunctor D) (FOp * F))
-    := (Build_SpecializedNaturalTransformation (HomFunctor C) (ComposeFunctors (HomFunctor D) (FOp * F))
-                                               (fun sd : (COp * C) =>
-                                                  MorphismOf F (s := _) (d := _))).
-End FullFaithful.
-
-Definition FunctorCategory
-           `(C : @SpecializedCategory objC)
-           `(D : @SpecializedCategory objD)
-: @SpecializedCategory (SpecializedFunctor C D).
-  refine (@Build_SpecializedCategory _
-                                     (SpecializedNaturalTransformation (C := C) (D := D))
-                                     _);
-  admit.
-Defined.
-
-Notation "C ^ D" := (FunctorCategory D C) : category_scope.
-
-Section Yoneda.
-  Context `(C : @SpecializedCategory objC).
-  Let COp := OppositeCategory C.
-
-  Section Yoneda.
-    Let Yoneda_NT s d (f : COp.(Morphism) s d) : SpecializedNaturalTransformation (CovariantHomFunctor C s) (CovariantHomFunctor C d)
-      := Build_SpecializedNaturalTransformation
-           (CovariantHomFunctor C s)
-           (CovariantHomFunctor C d)
-           (fun c : C => (fun m : C.(Morphism) _ _ => Compose m f)).
-
-    Definition Yoneda : SpecializedFunctor COp (TypeCat ^ C)
-      := Build_SpecializedFunctor COp (TypeCat ^ C)
-                                  (fun c : COp => CovariantHomFunctor C c : TypeCat ^ C)
-                                  (fun s d (f : Morphism COp s d) => Yoneda_NT s d f).
-  End Yoneda.
-End Yoneda.
-
-Section FullyFaithful.
-  Context `(C : @SpecializedCategory objC).
-
-  Set Printing Universes.
-  Fail Check InducedHomNaturalTransformation (Yoneda C).
-  (* Error: Universe inconsistency (cannot enforce Top.865 = Top.851 because
-Top.851 < Top.869 <= Top.864 <= Top.865). *)
-End FullyFaithful.
diff --git a/test-suite/bugs/opened/HoTT_coq_032.v b/test-suite/bugs/opened/HoTT_coq_032.v
deleted file mode 100644
index e6ae8a0c4f..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_032.v
+++ /dev/null
@@ -1,22 +0,0 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-xml") -*- *)
-Set Implicit Arguments.
-Generalizable All Variables.
-Set Asymmetric Patterns.
-Set Universe Polymorphism.
-
-Delimit Scope object_scope with object.
-Delimit Scope morphism_scope with morphism.
-Delimit Scope category_scope with category.
-Delimit Scope functor_scope with functor.
-
-Local Open Scope category_scope.
-
-Fail Record SpecializedCategory (obj : Type) :=
-  {
-    Object :> _ := obj;
-    Morphism : obj -> obj -> Type;
-
-    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
-  }.
-(* Anomaly: Mismatched instance and context when building universe substitution.
-Please report. *)