HoTT/coq bug #7 is closed, and the definitions can be made to go through using explicit

universes. The behavior of Hint Rewrite still differs from Hint Resolve though.

1 files changed, 0 insertions, 115 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_007.v b/test-suite/bugs/opened/HoTT_coq_007.v
deleted file mode 100644
index f609aff5d..000000000
--- a/test-suite/bugs/opened/HoTT_coq_007.v
+++ /dev/null
@@ -1,115 +0,0 @@
-Module Comment1.
-  Set Implicit Arguments.
-
-  Polymorphic Record Category (obj : Type) :=
-    {
-      Morphism : obj -> obj -> Type;
-      Identity : forall o, Morphism o o
-    }.
-
-  Polymorphic Record Functor objC (C :Category objC) objD (D : Category objD) :=
-    {
-      ObjectOf :> objC -> objD;
-      MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d);
-      FIdentityOf : forall o, MorphismOf _ _ (C.(Identity) o) = D.(Identity) (ObjectOf o)
-    }.
-
-  Create HintDb functor discriminated.
-
-  Hint Rewrite @FIdentityOf : functor.
-
-  Polymorphic Definition ComposeFunctors objC C objD D objE E (G : @Functor objD D objE E) (F : @Functor objC C objD D) : Functor C E.
-  refine {| ObjectOf := (fun c => G (F c));
-            MorphismOf := (fun _ _ m => G.(MorphismOf) _ _ (F.(MorphismOf) _ _ m))
-         |};
-    intros; autorewrite with functor; reflexivity.
-  Defined.
-
-  Definition Cat0 : Category Empty_set.
-    refine {|
-        Morphism := fun s d : Empty_set => s = d;
-        Identity := fun o : Empty_set => eq_refl
-      |};
-    admit.
-  Defined.
-
-  Set Printing All.
-  Set Printing Universes.
-
-  Fail Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x). (** ??? The term "y" has type
- "@Functor (* Top.448 Top.449 Top.450 Top.451 *)
-    (@Functor (* Set Top.441 Top.442 Top.336 *) Empty_set Cat0 objC C) C0
-    Empty_set Cat0" while it is expected to have type
- "@Functor (* Top.295 Top.296 Top.295 Top.296 *) ?46 ?47 ?48 ?49"
-(Universe inconsistency: Cannot enforce Set = Top.295)). *)
-  Fail intro. (* Illegal application (Type Error) *)
-  Fail Abort.
-End Comment1.
-
-Module Comment2.
-  Set Implicit Arguments.
-
-  Polymorphic Record Category (obj : Type) :=
-    {
-      Morphism : obj -> obj -> Type;
-
-      Identity : forall o, Morphism o o;
-      Compose : forall s d d2, Morphism d d2 -> Morphism s d -> Morphism s d2;
-
-      LeftIdentity : forall a b (f : Morphism a b), Compose (Identity b) f = f
-    }.
-
-  Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) :=
-    {
-      ObjectOf : objC -> objD;
-      MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
-    }.
-
-  Create HintDb morphism discriminated.
-
-  Polymorphic Hint Resolve @LeftIdentity : morphism.
-
-  Polymorphic Definition ProductCategory objC (C : Category objC) objD (D : Category objD) : @Category (objC * objD)%type.
-  refine {|
-      Morphism := (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type);
-      Identity := (fun o => (Identity _ (fst o), Identity _ (snd o)));
-      Compose := (fun (s d d2 : (objC * objD)%type) m2 m1 => (C.(Compose) _ _ _ (fst m2) (fst m1), D.(Compose) _ _ _ (snd m2) (snd m1)))
-    |};
-    intros; apply injective_projections; simpl; auto with morphism. (* Replacing [auto with morphism] with [apply @LeftIdentity] removes the error *)
-  Defined.
-
-  Polymorphic Definition Cat0 : Category Empty_set.
-  refine {|
-      Morphism := fun s d : Empty_set => s = d;
-      Identity := fun o : Empty_set => eq_refl;
-      Compose := fun s d d2 m0 m1 => eq_trans m1 m0
-    |};
-    admit.
-  Defined.
-
-  Set Printing All.
-  Set Printing Universes.
-  Polymorphic Definition ProductLaw0Functor (objC : Type) (C : Category objC) : Functor (ProductCategory C Cat0) Cat0.
-  refine (Build_Functor (ProductCategory C Cat0) Cat0 _ _). (* Toplevel input, characters 15-71:
-Error: Refiner was given an argument
- "prod (* Top.2289 Top.2289 *) objC Empty_set" of type
-"Type (* Top.2289 *)" instead of "Set". *)
-  Abort.
-  Polymorphic Definition ProductLaw0Functor (objC : Type) (C : Category objC) : Functor (ProductCategory C Cat0) Cat0.
-  econstructor. (* Toplevel input, characters 0-12:
-Error: No applicable tactic.
-                 *)
-  Abort.
-End Comment2.
-
-
-Module Comment3.
-  Polymorphic Lemma foo {obj : Type} : 1 = 1.
-  trivial.
-  Qed.
-
-  Polymorphic Hint Resolve foo. (* success *)
-  Polymorphic Hint Rewrite @foo. (* Success *)
-  Polymorphic Hint Resolve @foo. (* Error: @foo is a term and cannot be made a polymorphic hint, only global references can be polymorphic hints. *)
-  Fail Polymorphic Hint Rewrite foo. (* Error: Cannot infer the implicit parameter obj of foo. *)
-End Comment3.