Add regression tests for univ. poly. and prim proj

These regression tests are aggregated from the various bugs I (and
others) have reported on https://github.com/HoTT/coq/issues relating to
universe polymorphism, primitive projections, and eta for records.
These are the tests that trunk currently passes.

I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the
number of the issue in GitHub), but I couldn't think of a better one.

50 files changed, 2249 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/2250.v b/test-suite/bugs/closed/2250.v
new file mode 100644
index 000000000..565d7b68f
--- /dev/null
+++ b/test-suite/bugs/closed/2250.v
@@ -0,0 +1,3 @@
+Check prod: Prop -> Prop -> Prop.
+(* (fun A B : Prop => (A * B)%type):Prop -> Prop -> Prop
+     : Prop -> Prop -> Prop *)
diff --git a/test-suite/bugs/closed/3205.v b/test-suite/bugs/closed/3205.v
new file mode 100644
index 000000000..5c44f0703
--- /dev/null
+++ b/test-suite/bugs/closed/3205.v
@@ -0,0 +1,26 @@
+Fail Fixpoint F (u : unit) : Prop :=
+  (fun p : {P : Prop & _} => match p with existT _ _ P => P end)
+  (existT (fun P => False -> P) (F tt) _).
+(* Anomaly: A universe comparison can only happen between variables.
+Please report. *)
+
+
+
+Definition g (x : Prop) := x.
+
+Definition h (y : Type) := y.
+
+Definition eq_hf : h = g :> (Prop -> Type) :=
+  @eq_refl (Prop -> Type) g.
+
+Set Printing All.
+Set Printing Universes.
+Fail Definition eq_hf : h = g :> (Prop -> Type) :=
+  eq_refl g.
+(* Originally an anomaly, now says
+Toplevel input, characters 48-57:
+Error:
+The term "@eq_refl (forall _ : Prop, Prop) g" has type
+ "@eq (forall _ : Prop, Prop) g g" while it is expected to have type
+ "@eq (forall _ : Prop, Type (* Top.16 *)) (fun y : Prop => h y) g"
+(Universe inconsistency: Cannot enforce Prop = Top.16)). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_001.v b/test-suite/bugs/closed/HoTT_coq_001.v
new file mode 100644
index 000000000..bf1d024b2
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_001.v
@@ -0,0 +1,5 @@
+Record Foo : Set :=
+  {
+    A' : nat;
+    A : Prop := (A' = 0)
+  }. (* Anomaly: Uncaught exception Reduction.NotConvertible. Please report. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_002.v b/test-suite/bugs/closed/HoTT_coq_002.v
new file mode 100644
index 000000000..ba69f6b15
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_002.v
@@ -0,0 +1,33 @@
+Set Implicit Arguments.
+
+Generalizable All Variables.
+
+Parameter SpecializedCategory : Type -> Type.
+Parameter Object : forall obj, SpecializedCategory obj -> Type.
+
+Section SpecializedFunctor.
+  (* Variable objC : Type. *)
+  Context `(C : SpecializedCategory objC).
+
+  Polymorphic Record SpecializedFunctor := {
+    ObjectOf' : objC -> Type;
+    ObjectC : Object C
+  }.
+End SpecializedFunctor.
+
+Section FunctorInterface.
+  Variable objC : Type.
+  Variable C : SpecializedCategory objC.
+  Variable F : SpecializedFunctor C.
+
+  Set Printing All.
+  Set Printing Universes.
+  Check @ObjectOf' objC C F. (* Toplevel input, characters 24-25:
+Error:
+In environment
+objC : Type (* Top.515 *)
+C : SpecializedCategory objC
+F : @SpecializedFunctor (* Top.516 *) objC C
+The term "F" has type "@SpecializedFunctor (* Top.516 *) objC C"
+ while it is expected to have type
+ "@SpecializedFunctor (* Top.519 Top.520 *) objC C". *)
diff --git a/test-suite/bugs/closed/HoTT_coq_006.v b/test-suite/bugs/closed/HoTT_coq_006.v
new file mode 100644
index 000000000..c7943b840
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_006.v
@@ -0,0 +1,99 @@
+Module FirstIssue.
+  Set Implicit Arguments.
+
+  Record Cat (obj : Type) := {}.
+
+  Record Functor objC (C : Cat objC) objD (D : Cat objD) :=
+    {
+      ObjectOf' : objC -> objD
+    }.
+
+  Definition TypeCat : Cat Type. constructor. Defined.
+  Definition PropCat : Cat Prop. constructor. Defined.
+
+  Definition FunctorFrom_Type2Prop objC (C : Cat objC) (F : Functor TypeCat C) : Functor PropCat C.
+    Set Printing All.
+    Set Printing Universes.
+    Check F. (* F : @Functor Type (* Top.1201 *) TypeCat objC C *)
+    exact (Build_Functor PropCat C (ObjectOf' F)).
+    Show Proof. (* (fun (objC : Type (* Top.1194 *)) (C : Cat objC)
+   (F : @Functor Prop TypeCat objC C) =>
+ @Build_Functor Prop PropCat objC C
+   (@ObjectOf' Prop TypeCat objC C F)) *)
+  Defined.
+  (* Error: Illegal application (Type Error):
+The term "Functor" of type
+ "forall (objC : Type (* Top.1194 *)) (_ : Cat objC)
+    (objD : Type (* Top.1194 *)) (_ : Cat objD),
+  Type (* Top.1194 *)"
+cannot be applied to the terms
+ "Prop" : "Type (* (Set)+1 *)"
+ "TypeCat" : "Cat Type (* Top.1201 *)"
+ "objC" : "Type (* Top.1194 *)"
+ "C" : "Cat objC"
+The 2nd term has type "Cat Type (* Top.1201 *)"
+which should be coercible to "Cat Prop". *)
+End FirstIssue.
+
+Module SecondIssue.
+  Set Implicit Arguments.
+
+  Set Printing Universes.
+
+  Polymorphic Record Cat (obj : Type) :=
+    {
+      Object :> _ := obj;
+      Morphism' : obj -> obj -> Type
+    }.
+
+  Polymorphic Record Functor objC (C : Cat objC) objD (D : Cat objD) :=
+    {
+      ObjectOf' : objC -> objD;
+      MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d)
+    }.
+
+  Definition SetCat : Cat Set := @Build_Cat Set (fun x y => x -> y).
+  Definition PropCat : Cat Prop := @Build_Cat Prop (fun x y => x -> y).
+
+  Set Printing All.
+
+  Definition FunctorFrom_Set2Prop objC (C : Cat objC) (F : Functor SetCat C) : Functor PropCat C.
+    exact (Build_Functor PropCat C
+                         (ObjectOf' F)
+                         (MorphismOf' F)
+          ).
+  Defined. (* Error: Illegal application (Type Error):
+The term "Build_Functor (* Top.748 Prop Top.808 Top.809 *)" of type
+ "forall (objC : Type (* Top.748 *)) (C : Cat (* Top.748 Prop *) objC)
+    (objD : Type (* Top.808 *)) (D : Cat (* Top.808 Top.809 *) objD)
+    (ObjectOf' : forall _ : objC, objD)
+    (_ : forall (s d : objC) (_ : @Morphism' (* Top.748 Prop *) objC C s d),
+         @Morphism' (* Top.808 Top.809 *) objD D (ObjectOf' s) (ObjectOf' d)),
+  @Functor (* Top.748 Prop Top.808 Top.809 *) objC C objD D"
+cannot be applied to the terms
+ "Prop" : "Type (* (Set)+1 *)"
+ "PropCat" : "Cat (* Top.748 Prop *) Prop"
+ "objC" : "Type (* Top.808 *)"
+ "C" : "Cat (* Top.808 Top.809 *) objC"
+ "fun x : Prop =>
+  @ObjectOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F x"
+   : "forall _ : Prop, objC"
+ "@MorphismOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F"
+   : "forall (s d : Set) (_ : @Morphism' (* Top.744 Prop *) Set SetCat s d),
+      @Morphism' (* Top.808 Top.809 *) objC C
+        (@ObjectOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F s)
+        (@ObjectOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F d)"
+The 6th term has type
+ "forall (s d : Set) (_ : @Morphism' (* Top.744 Prop *) Set SetCat s d),
+  @Morphism' (* Top.808 Top.809 *) objC C
+    (@ObjectOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F s)
+    (@ObjectOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F d)"
+which should be coercible to
+ "forall (s d : Prop) (_ : @Morphism' (* Top.748 Prop *) Prop PropCat s d),
+  @Morphism' (* Top.808 Top.809 *) objC C
+    ((fun x : Prop =>
+      @ObjectOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F x) s)
+    ((fun x : Prop =>
+      @ObjectOf' (* Top.744 Prop Top.808 Top.809 *) Set SetCat objC C F x) d)".
+            *)
+End SecondIssue.
diff --git a/test-suite/bugs/closed/HoTT_coq_010.v b/test-suite/bugs/closed/HoTT_coq_010.v
new file mode 100644
index 000000000..42b1244fb
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_010.v
@@ -0,0 +1,3 @@
+SearchAbout and.
+(* Anomaly: Mismatched instance and context when building universe substitution.
+Please report. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_012.v b/test-suite/bugs/closed/HoTT_coq_012.v
new file mode 100644
index 000000000..a3c697f8c
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_012.v
@@ -0,0 +1,4 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+
+Definition UU := Type.
+Inductive toto (B : UU) : UU := c (x : B).
diff --git a/test-suite/bugs/closed/HoTT_coq_013.v b/test-suite/bugs/closed/HoTT_coq_013.v
new file mode 100644
index 000000000..cc5ed8626
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_013.v
@@ -0,0 +1,24 @@
+Set Implicit Arguments.
+Generalizable All Variables.
+
+Polymorphic Record Category (obj : Type) :=.
+
+            Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) :=.
+
+            Polymorphic Definition ComposeFunctors objC C objD D objE E (G : @Functor objD D objE E) (F : @Functor objC C objD D) : Functor C E.
+Admitted.
+
+Polymorphic Definition ProductCategory objC (C : Category objC) objD (D : Category objD) : @Category (objC * objD)%type.
+Admitted.
+
+Polymorphic Definition Cat0 : Category Empty_set.
+Admitted.
+
+Set Printing Universes.
+
+Lemma ProductLaw0 objC (C : Category objC) (F : Functor (ProductCategory C Cat0) Cat0) (G : Functor Cat0 (ProductCategory C Cat0)) x y :
+  ComposeFunctors F G = x /\
+  ComposeFunctors G F = y.
+Proof.
+  split. (* Error: Refiner was given an argument "(objC * 0)%type" of type "Type" instead of "Set". *)
+Abort.
diff --git a/test-suite/bugs/closed/HoTT_coq_016.v b/test-suite/bugs/closed/HoTT_coq_016.v
new file mode 100644
index 000000000..4f12cf1a9
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_016.v
@@ -0,0 +1,15 @@
+Set Printing Universes.
+Local Close Scope nat_scope.
+Check (fun ab : Prop * Prop => (fst ab : Prop) * (snd ab : Prop)).
+(* fun ab : Prop * Prop =>
+(fst (* Top.5817 Top.5818 *) ab:Prop) * (snd (* Top.5817 Top.5818 *) ab:Prop)
+     : Prop * Prop -> Prop *)
+Check (fun ab : Prop * Prop => (fst ab : Prop) * (snd ab : Prop) : Prop).
+(* Toplevel input, characters 51-84:
+Error: In environment
+ab : Prop * Prop
+The term
+ "(fst (* Top.5833 Top.5834 *) ab:Prop) *
+  (snd (* Top.5833 Top.5834 *) ab:Prop)" has type
+ "Type (* max(Top.5829, Top.5830) *)" while it is expected to have type
+ "Prop". *)
diff --git a/test-suite/bugs/closed/HoTT_coq_023.v b/test-suite/bugs/closed/HoTT_coq_023.v
new file mode 100644
index 000000000..b52140de1
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_023.v
@@ -0,0 +1,12 @@
+Set Universe Polymorphism.
+
+Record Type_Over (X : Type)
+:= { Domain :> Type;
+     proj : Domain -> X }.
+
+Definition Self_Over (X : Type)
+  := {| Domain := X; proj := (fun x => x) |}.
+
+Canonical Structure Self_Over. (* fails with Anomaly: Mismatched instance and context when building universe substitution. Please report. for polymorphic structures *)
+(* if monomorphic, Warning: No global reference exists for projection
+ valuefun x : _UNBOUND_REL_1 => x in instance Self_Over of proj, ignoring it. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_025.v b/test-suite/bugs/closed/HoTT_coq_025.v
new file mode 100644
index 000000000..b81b454d0
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_025.v
@@ -0,0 +1,29 @@
+Module monomorphic.
+  Class Inhabited (A : Type) : Prop := populate { _ : A }.
+  Arguments populate {_} _.
+
+  Instance prod_inhabited {A B : Type} (iA : Inhabited A)
+           (iB : Inhabited B) :   Inhabited (A * B) :=
+    match iA, iB with
+      | populate x, populate y => populate (x,y)
+    end.
+  (* Error: In environment
+A : Type
+B : Type
+iA : Inhabited A
+iB : Inhabited B
+The term "(A * B)%type" has type "Type" while it is expected to have type
+"Prop". *)
+End monomorphic.
+
+Module polymorphic.
+  Set Universe Polymorphism.
+  Class Inhabited (A : Type) : Prop := populate { _ : A }.
+  Arguments populate {_} _.
+
+  Instance prod_inhabited {A B : Type} (iA : Inhabited A)
+           (iB : Inhabited B) :   Inhabited (A * B) :=
+    match iA, iB with
+      | populate x, populate y => populate (x,y)
+    end.
+End polymorphic.
diff --git a/test-suite/bugs/closed/HoTT_coq_028.v b/test-suite/bugs/closed/HoTT_coq_028.v
new file mode 100644
index 000000000..b03241402
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_028.v
@@ -0,0 +1,14 @@
+Goal forall (O obj : Type) (f : O -> obj) (x : O) (e : x = x)
+     (T : obj -> obj -> Type) (m : forall x0 : obj, T x0 x0),
+   match eq_sym e in (_ = y) return (T (f y) (f x)) with
+   | eq_refl => m (f x)
+   end = m (f x).
+intros.
+try case e.
+(* Toplevel input, characters 19-25:
+Error: Cannot instantiate metavariable P of type
+"forall a : O, x = a -> Prop" with abstraction
+"fun (x : O) (e : x = x) =>
+ match eq_sym e in (_ = y) return (T (f y) (f x)) with
+ | eq_refl => m (f x)
+ end = m (f x)" of incompatible type "forall x : O, x = x -> Prop". *)
diff --git a/test-suite/bugs/closed/HoTT_coq_035.v b/test-suite/bugs/closed/HoTT_coq_035.v
new file mode 100644
index 000000000..4ad2fc023
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_035.v
@@ -0,0 +1,19 @@
+Fail Check Prop : Prop. (* Prop:Prop
+     : Prop *)
+Fail Check Set : Prop. (* Set:Prop
+     : Prop *)
+Fail Check ((bool -> Prop) : Prop). (* bool -> Prop:Prop
+     : Prop *)
+Axiom proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2.
+Check ((True : Prop) : Set). (* (True:Prop):Set
+     : Set *)
+Goal (forall (v : Type) (f1 f0 : v -> Prop),
+        @eq (v -> Prop) f0 f1).
+intros.
+Fail apply proof_irrelevance.
+admit.
+Defined. (* Unnamed_thm is defined *)
+Set Printing Universes.
+Check ((True : Prop) : Set). (* Toplevel input, characters 0-28:
+Error: Universe inconsistency (cannot enforce Prop <= Set because Set
+< Prop). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_037.v b/test-suite/bugs/closed/HoTT_coq_037.v
new file mode 100644
index 000000000..664764146
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_037.v
@@ -0,0 +1,16 @@
+Set Printing Universes.
+
+Fixpoint CardinalityRepresentative (n : nat) : Set :=
+  match n with
+    | O => Empty_set
+    | S n' => sum (CardinalityRepresentative n') unit
+  end.
+(* Toplevel input, characters 104-143:
+Error:
+In environment
+CardinalityRepresentative : nat -> Set
+n : nat
+n' : nat
+The term "(CardinalityRepresentative n' + unit)%type" has type
+ "Type (* max(Top.73, Top.74) *)" while it is expected to have type
+"Set". *)
diff --git a/test-suite/bugs/closed/HoTT_coq_041.v b/test-suite/bugs/closed/HoTT_coq_041.v
new file mode 100644
index 000000000..79933bb85
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_041.v
@@ -0,0 +1,18 @@
+Set Printing All.
+Definition foo (s d : Prop)
+ : ((s : Set) -> (d : Set)) = ((s : Prop) -> (d : Prop))
+ := eq_refl. (* succeeds *)
+Definition bar (s d : Prop)
+ : ((fun x : Set => x) s -> (fun x : Set => x) d) = ((fun x : Prop => x) s -> (fun x : Prop => x) d)
+ := eq_refl. (* Toplevel input, characters 131-138:
+Error:
+In environment
+s : Prop
+d : Prop
+The term
+ "@eq_refl Set (forall _ : (fun x : Set => x) s, (fun x : Set => x) d)"
+has type "@eq Set (forall _ : s, d) (forall _ : s, d)"
+while it is expected to have type
+ "@eq Set (forall _ : s, d) (forall _ : s, d)"
+(cannot unify "forall _ : (fun x : Set => x) s, (fun x : Set => x) d" and
+"forall _ : (fun x : Prop => x) s, (fun x : Prop => x) d"). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_042.v b/test-suite/bugs/closed/HoTT_coq_042.v
new file mode 100644
index 000000000..6b206a2f5
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_042.v
@@ -0,0 +1,27 @@
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Generalizable All Variables.
+
+Record Category (obj : Type) := { Morphism : obj -> obj -> Type }.
+
+Definition SetCat : @Category Set := @Build_Category Set (fun s d => s -> d).
+
+Record Foo := { foo : forall A (f : Morphism SetCat A A), True }.
+
+Local Notation PartialBuild_Foo pf := (@Build_Foo (fun A f => pf A f)).
+
+Set Printing Universes.
+Let SetCatFoo' : Foo.
+  let pf := fresh in
+  let pfT := fresh in
+  evar (pfT : Prop);
+    cut pfT;
+    [ subst pfT; intro pf;
+      let t := constr:(PartialBuild_Foo pf) in
+      let t' := (eval simpl in t) in
+      exact t'
+    | ].
+  admit.
+(* Toplevel input, characters 15-20:
+Error: Universe inconsistency (cannot enforce Set <= Prop).
+ *)
diff --git a/test-suite/bugs/closed/HoTT_coq_043.v b/test-suite/bugs/closed/HoTT_coq_043.v
new file mode 100644
index 000000000..5257a0322
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_043.v
@@ -0,0 +1,15 @@
+Require Import Classes.RelationClasses List Setoid.
+
+Definition RowType := list Type.
+
+Inductive RowTypeDecidable (P : forall T, relation T) `(forall T, Equivalence (P T))
+: RowType -> Type :=
+| RTDecNil : RowTypeDecidable P _ nil
+| RTDecCons : forall T Ts, (forall t0 t1 : T,
+                              {P T t0 t1} + {~P T t0 t1})
+                           -> RowTypeDecidable P _ Ts
+                           -> RowTypeDecidable P _ (T :: Ts).
+(* Toplevel input, characters 15-378:
+Error:
+Last occurrence of "RowTypeDecidable" must have "H" as 2nd argument in
+ "RowTypeDecidable P (fun T : Type => H T) nil". *)
diff --git a/test-suite/bugs/closed/HoTT_coq_044.v b/test-suite/bugs/closed/HoTT_coq_044.v
new file mode 100644
index 000000000..1a59de092
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_044.v
@@ -0,0 +1,32 @@
+Require Import Classes.RelationClasses List Setoid.
+
+Set Universe Polymorphism.
+
+Definition RowType := list Type.
+
+
+Inductive Row : RowType -> Type :=
+| RNil : Row nil
+| RCons : forall T Ts, T -> Row Ts -> Row (T :: Ts).
+
+Inductive RowTypeDecidable (P : forall T, relation T) `(H : forall T, Equivalence (P T))
+: RowType -> Type :=
+| RTDecNil : RowTypeDecidable P H nil
+| RTDecCons : forall T Ts, (forall t0 t1 : T,
+                              {P T t0 t1} + {~P T t0 t1})
+                           -> RowTypeDecidable P H Ts
+                           -> RowTypeDecidable P H (T :: Ts).
+
+Set Printing Universes.
+
+Fixpoint Row_eq Ts
+: RowTypeDecidable (@eq) _ Ts -> forall r1 r2 : Row Ts, {@eq (Row Ts) r1 r2} + {r1 <> r2}.
+(* Toplevel input, characters 81-87:
+Error:
+In environment
+Ts : RowType (* Top.53 Coq.Init.Logic.8 *)
+r1 : Row (* Top.54 Top.55 *) Ts
+r2 : Row (* Top.56 Top.57 *) Ts
+The term "Row (* Coq.Init.Logic.8 Top.59 *) Ts" has type
+ "Type (* max(Top.58+1, Top.59) *)" while it is expected to have type
+ "Type (* Coq.Init.Logic.8 *)" (Universe inconsistency). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_047.v b/test-suite/bugs/closed/HoTT_coq_047.v
new file mode 100644
index 000000000..29496be5e
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_047.v
@@ -0,0 +1,46 @@
+Inductive nCk : nat -> nat -> Type :=
+  |zz : nCk 0 0
+  | incl { m n : nat } : nCk m n -> nCk (S m) (S n)
+  | excl { m n : nat } : nCk m n -> nCk (S m) n.
+
+Definition nCkComp { l m n : nat } :
+  nCk l m -> nCk m n -> nCk l n.
+Proof.
+  intro.
+  revert n.
+  induction H.
+  auto.
+(* ( incl w ) o zz -> contradiction *)
+  intros.
+    remember (S n) as sn.
+    destruct H0.
+      discriminate Heqsn.
+    apply incl.
+      apply IHnCk.
+      injection Heqsn.
+      intro.
+      rewrite <- H1.
+      auto.
+    apply excl.
+      apply IHnCk.
+      injection Heqsn.
+      intro. rewrite <- H1.
+      auto.
+  intros.
+  apply excl.
+  apply IHnCk.
+  auto.
+Defined.
+
+Lemma nCkEq { k l m n : nat } ( cs : nCk k l ) (ct : nCk l m) (cr : nCk m n ):
+  nCkComp cs (nCkComp ct cr) = nCkComp (nCkComp cs ct) cr.
+Proof.
+  revert m n ct cr.
+  induction cs.
+  intros. simpl. auto.
+  intros.
+  destruct n.
+   destruct m0.
+    destruct n0.
+     destruct cr.
+(* Anomaly: Evar ?nnn was not declared. Please report. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_048.v b/test-suite/bugs/closed/HoTT_coq_048.v
new file mode 100644
index 000000000..831bb3fc4
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_048.v
@@ -0,0 +1,7 @@
+(** This is not the issue of https://github.com/HoTT/coq/issues/48, but was mentioned there. *)
+Record Foo :=
+  {
+    foo := 1;
+    bar : foo = foo
+  }.
+(* Anomaly: lookup_projection: constant is not a projection. Please report. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_049.v b/test-suite/bugs/closed/HoTT_coq_049.v
new file mode 100644
index 000000000..906ec329e
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_049.v
@@ -0,0 +1,6 @@
+Require Import FunctionalExtensionality.
+
+Goal forall y, @f_equal = y.
+intro.
+apply functional_extensionality_dep.
+(* Error: Ill-typed evar instance in HoTT/coq, Anomaly: Uncaught exception Reductionops.NotASort(_). Please report. before that. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_050.v b/test-suite/bugs/closed/HoTT_coq_050.v
new file mode 100644
index 000000000..ce9b6b297
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_050.v
@@ -0,0 +1,33 @@
+Set Implicit Arguments.
+Generalizable All Variables.
+Set Asymmetric Patterns.
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Set Printing All.
+
+Record PreCategory :=
+  {
+    Object :> Type;
+    Morphism : Object -> Object -> Type
+  }.
+
+Inductive paths A (x : A) : A -> Type := idpath : @paths A x x.
+Inductive Unit : Prop := tt. (* Changing this to [Set] fixes things *)
+Inductive Bool : Set := true | false.
+
+Definition DiscreteCategory X : PreCategory
+  := @Build_PreCategory X
+                        (@paths X).
+
+Definition IndiscreteCategory X : PreCategory
+  := @Build_PreCategory X
+                        (fun _ _ => Unit).
+
+Check (IndiscreteCategory Unit).
+Check (DiscreteCategory Bool).
+Definition NatCategory (n : nat) :=
+  match n with
+    | 0 => IndiscreteCategory Unit
+    | _ => DiscreteCategory Bool
+  end. (* Error: Universe inconsistency (cannot enforce Set <= Prop). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_055.v b/test-suite/bugs/closed/HoTT_coq_055.v
new file mode 100644
index 000000000..92d70ad13
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_055.v
@@ -0,0 +1,53 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+Set Universe Polymorphism.
+
+Inductive Empty : Prop := .
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Arguments idpath {A a} , [A] a.
+
+Definition idmap {A : Type} : A -> A := fun x => x.
+
+Definition path_sum {A B : Type} (z z' : A + B)
+           (pq : match z, z' with
+                   | inl z0, inl z'0 => z0 = z'0
+                   | inr z0, inr z'0 => z0 = z'0
+                   | _, _ => Empty
+                 end)
+: z = z'.
+
+  admit.
+Defined.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
+
+        (pq : match (x, y) with (inl x', inl y') => x' = y' | (inr x', inr y') => x' = y' | _ => Empty end) :
+  let f z := match z with inl z' => inl (g z') | inr z' => inr (h z') end in
+  ap f (path_sum x y pq) = path_sum (f x) (f y)
+                                    ((match x as x return match (x, y) with
+                                                              (inl x', inl y') => x' = y'
+                                                            | (inr x', inr y') => x' = y'
+                                                            | _ => Empty
+                                                          end -> match (f x, f y) with
+                                                                   | (inl x', inl y') => x' = y'
+                                                                   | (inr x', inr y') => x' = y'
+                                                                   | _ => Empty end with
+                                        | inl x' => match y with
+                                                      | inl y' => ap g
+                                                      | inr y' => idmap
+                                                    end
+                                        | inr x' => match y with
+                                                      | inl y' => idmap
+                                                      | inr y' => ap h
+                                                    end
+                                      end) pq).
+
+Admitted.
+(* Toplevel input, characters 20-29:
+Error: Matching on term "f y" of type "A' + B'" expects 2 branches. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v
new file mode 100644
index 000000000..6e65320d1
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_056.v
@@ -0,0 +1,156 @@
+(* File reduced by coq-bug-finder from 10455 lines to 8350 lines, then from 7790 lines to 710 lines, then from 7790 lines to 710 lines, then from 566 lines to 340 lines, then from 191 lines to 171 lines, then from 191 lines to 171 lines. *)
+
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Definition admit {T} : T.
+Admitted.
+Reserved Notation "x ≅ y" (at level 70, no associativity).
+Reserved Notation "i ^op" (at level 3).
+Reserved Infix "∘" (at level 40, left associativity).
+Reserved Notation "F ⟨ x ⟩" (at level 10, no associativity, x at level 10).
+Reserved Notation "F ⟨ x , y ⟩" (at level 10, no associativity, x at level 10, y at level 10).
+Reserved Notation "F ⟨ ─ ⟩" (at level 10, no associativity).
+Reserved Notation "F ⟨ x , ─ ⟩" (at level 10, no associativity, x at level 10).
+Reserved Notation "F ⟨ ─ , y ⟩" (at level 10, no associativity, y at level 10).
+Delimit Scope object_scope with object.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope functor_scope with functor.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Delimit Scope path_scope with path.
+Local Open Scope path_scope.
+
+Record PreCategory :=
+  Build_PreCategory' {
+      Object :> Type;
+      Morphism : Object -> Object -> Type
+    }.
+
+Bind Scope category_scope with PreCategory.
+
+Definition Build_PreCategory
+           Object Morphism
+  := @Build_PreCategory' Object
+                         Morphism.
+
+Record Functor (C D : PreCategory) :=
+  {
+    ObjectOf :> C -> D;
+    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
+  }.
+Arguments MorphismOf [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
+Class Isomorphic {C : PreCategory} (s d : C) := {}.
+Definition ComposeFunctors C D E (G : Functor D E) (F : Functor C D) : Functor C E
+  := Build_Functor C E
+                   (fun c => G (F c))
+                   (fun _ _ m => G.(MorphismOf) (F.(MorphismOf) m)).
+
+Infix "∘" := ComposeFunctors : functor_scope.
+
+Definition IdentityFunctor C : Functor C C
+  := Build_Functor C C
+                   (fun x => x)
+                   (fun _ _ x => x).
+
+Notation "─" := (IdentityFunctor _) : functor_scope.
+Record NaturalTransformation C D (F G : Functor C D) :=
+  Build_NaturalTransformation' { }.
+
+Definition OppositeCategory (C : PreCategory) : PreCategory
+  := @Build_PreCategory' C
+                         (fun s d => Morphism C d s).
+
+Notation "C ^op" := (OppositeCategory C) : category_scope.
+
+Definition ProductCategory (C D : PreCategory) : PreCategory
+  := @Build_PreCategory (C * D)%type
+                        (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type).
+
+Infix "*" := ProductCategory : category_scope.
+
+Definition OppositeFunctor C D (F : Functor C D) : Functor (C ^op) (D ^op)
+  := Build_Functor (C ^op) (D ^op)
+                   (ObjectOf F)
+                   (fun s d => MorphismOf F (s := d) (d := s)).
+Notation "F ^op" := (OppositeFunctor F) : functor_scope.
+
+Definition FunctorProduct' C D C' D' (F : Functor C D) (F' : Functor C' D') : Functor (C * C') (D * D')
+  := admit.
+
+Global Class FunctorApplicationInterpretable
+       {C D} (F : Functor C D)
+       {argsT : Type} (args : argsT)
+       {T : Type} (rtn : T)
+  := {}.
+Definition FunctorApplicationOf {C D} F {argsT} args {T} {rtn}
+           `{@FunctorApplicationInterpretable C D F argsT args T rtn}
+  := rtn.
+
+Global Arguments FunctorApplicationOf / {C} {D} F {argsT} args {T} {rtn} {_}.
+
+Global Instance FunctorApplicationDash C D (F : Functor C D)
+: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0.
+Global Instance FunctorApplicationFunctorFunctor' A B C C' D (F : Functor (A * B) D) (G : Functor C A) (H : Functor C' B)
+: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100.
+
+Notation "F ⟨ x ⟩" := (FunctorApplicationOf F%functor x%functor) : functor_scope.
+
+Notation "F ⟨ x , y ⟩" := (FunctorApplicationOf F%functor (x%functor , y%functor)) : functor_scope.
+
+Notation "F ⟨ ─ ⟩" := (F ⟨ ( ─ ) ⟩)%functor : functor_scope.
+
+Notation "F ⟨ x , ─ ⟩" := (F ⟨ x , ( ─ ) ⟩)%functor : functor_scope.
+
+Notation "F ⟨ ─ , y ⟩" := (F ⟨ ( ─ ) , y ⟩)%functor : functor_scope.
+
+Definition FunctorCategory (C D : PreCategory) : PreCategory
+  := @Build_PreCategory (Functor C D)
+                        (NaturalTransformation (C := C) (D := D)).
+
+Notation "[ C , D ]" := (FunctorCategory C D) : category_scope.
+
+Definition SetCat : PreCategory := @Build_PreCategory Type (fun x y => x -> y).
+
+Definition HomFunctor C : Functor (C^op * C) SetCat.
+admit.
+Defined.
+Definition NaturalIsomorphism (C D : PreCategory) F G := @Isomorphic [C, D] F G.
+Infix "≅" := NaturalIsomorphism : natural_transformation_scope.
+
+Local Open Scope functor_scope.
+Local Open Scope natural_transformation_scope.
+
+Section Adjunction.
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+
+  Variable F : Functor C D.
+  Variable G : Functor D C.
+  Let Adjunction_Type := Eval simpl in HomFunctor D ⟨ F^op ⟨ ─ ⟩ , ─ ⟩ ≅ HomFunctor C ⟨ ─ , G ⟨ ─ ⟩ ⟩.
+  Record Adjunction := { AMateOf : Adjunction_Type }.
+End Adjunction.
+
+Section AdjunctionEquivalences.
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+
+  Variable F : Functor C D.
+  Variable G : Functor D C.
+  Variable A : Adjunction F G.
+  Set Printing All.
+  Definition foo := @AMateOf C D F G A.
+(* File "./HoTT_coq_56.v", line 145, characters 37-38:
+Error:
+In environment
+C : PreCategory
+D : PreCategory
+F : Functor C D
+G : Functor D C
+A : @Adjunction C D F G
+The term "A" has type "@Adjunction C D F G" while it is expected to have type
+ "@Adjunction C D F G". *)
+End AdjunctionEquivalences.
diff --git a/test-suite/bugs/closed/HoTT_coq_057.v b/test-suite/bugs/closed/HoTT_coq_057.v
new file mode 100644
index 000000000..e72ce0c5e
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_057.v
@@ -0,0 +1,33 @@
+Require Export Coq.Lists.List.
+
+Polymorphic Fixpoint LIn (A : Type) (a:A) (l:list A) : Type :=
+  match l with
+    | nil => False
+    | b :: m => (b = a) + LIn A a m
+  end.
+
+Polymorphic Inductive NTerm : Type :=
+| cterm : NTerm
+| oterm : list NTerm -> NTerm.
+
+Polymorphic Fixpoint dummy {A B} (x : list (A * B)) : list (A * B) :=
+  match x with
+    | nil => nil
+    | (_, _) :: _ => nil
+  end.
+
+Lemma foo :
+  forall v t sub vars,
+    LIn (nat * NTerm) (v, t) (dummy sub)
+    ->
+    (
+      LIn (nat * NTerm) (v, t) sub
+      *
+      notT (LIn nat v vars)
+    ).
+Proof.
+  induction sub; simpl; intros.
+  destruct H.
+  Set Printing Universes.
+  try (apply IHsub in X). (* Toplevel input, characters 5-21:
+Error: Universe inconsistency (cannot enforce Top.47 = Set). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_058.v b/test-suite/bugs/closed/HoTT_coq_058.v
new file mode 100644
index 000000000..9ce7dba97
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_058.v
@@ -0,0 +1,140 @@
+(* File reduced by coq-bug-finder from 10044 lines to 493 lines, then from 425 lines to 160 lines. *)
+Set Universe Polymorphism.
+Notation idmap := (fun x => x).
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+Open Scope fibration_scope.
+Notation "x .1" := (projT1 x) (at level 3) : fibration_scope.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Delimit Scope path_scope with path.
+Local Open Scope path_scope.
+
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
+: forall x, f x = g x
+  := fun x => match h with idpath => idpath end.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }.
+
+Delimit Scope equiv_scope with equiv.
+Local Open Scope equiv_scope.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
+
+Class Funext := { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+
+Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
+  (forall x, f x = g x) -> f = g
+  := (@apD10 A P f g)^-1.
+
+Inductive Unit : Set :=
+  tt : Unit.
+
+Definition path_prod_uncurried {A B : Type} (z z' : A * B)
+           (pq : (fst z = fst z') * (snd z = snd z'))
+: (z = z')
+  := match pq with (p,q) =>
+                   match z, z' return
+                         (fst z = fst z') -> (snd z = snd z') -> (z = z') with
+                     | (a,b), (a',b') => fun p q =>
+                                           match p, q with
+                                               idpath, idpath => idpath
+                                           end
+                   end p q
+     end.
+
+Definition path_prod {A B : Type} (z z' : A * B) :
+  (fst z = fst z') -> (snd z = snd z') -> (z = z')
+  := fun p q => path_prod_uncurried z z' (p,q).
+
+Definition path_prod' {A B : Type} {x x' : A} {y y' : B}
+: (x = x') -> (y = y') -> ((x,y) = (x',y'))
+  := fun p q => path_prod (x,y) (x',y') p q.
+
+Lemma path_forall_recr_beta `{Funext} A B x0 P f g e Px
+: @transport (forall a : A, B a)
+             (fun f => P f (f x0))
+             f
+             g
+             (@path_forall _ _ _ _ _ e)
+             Px
+  = @transport ((forall a, B a) * B x0)%type
+               (fun x => P (fst x) (snd x))
+               (f, f x0)
+               (g, g x0)
+               (path_prod' (@path_forall _ _ _ _ _ e) (e x0))
+               Px.
+
+  admit.
+Defined.
+Definition transport_path_prod'_beta' A B P (x x' : A) (y y' : B) (HA : x = x') (HB : y = y') (Px : P x y)
+: @transport (A * B) (fun xy => P (fst xy) (snd xy)) (x, y) (x', y') (@path_prod' A B x x' y y' HA HB) Px
+  = @transport A (fun x => P x y') x x' HA
+               (@transport B (fun y => P x y) y y' HB Px).
+  admit.
+Defined.
+Goal forall (T : Type) (T0 : T -> T -> Type)
+            (Pmor : forall s d : T, T0 s d -> Type) (x x0 : T)
+            (x1 : T0 x x0) (p : Pmor x x0 x1) (H : Funext),
+       transport
+         (fun x2 : {_ : T & Unit} -> {_ : T & Unit} =>
+            { x1 : _ & Pmor (x2 (x; tt)) .1 (x2 (x0; tt)) .1 x1})
+         (path_forall (fun c : {_ : T & Unit} => (c .1; tt)) idmap
+                      (fun x2 : {_ : T & Unit} =>
+                         let (x3, y) as s return ((s .1; tt) = s) := x2 in
+                         match y as y0 return ((x3; tt) = (x3; y0)) with
+                           | tt => idpath
+                         end)) (x1; p) = (x1; p).
+intros.
+let F := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(F) end in
+let H := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(H) end in
+let X := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(X) end in
+let T := match goal with |- appcontext[@transport _ (fun x0 => @?F x0) _ _ (@path_forall ?H ?X ?T ?f ?g ?e)] => constr:(T) end in
+let t0 := fresh "t0" in
+let t1 := fresh "t1" in
+let T1 := lazymatch type of F with (?T -> _) -> _ => constr:(T) end in
+    evar (t1 : T1);
+  let T0 := lazymatch type of F with (forall a : ?A, @?B a) -> ?C => constr:((forall a : A, B a) -> B t1 -> C) end in
+      evar (t0 : T0);
+
+    let dummy := fresh in
+    assert (dummy : forall x0, F x0 = t0 x0 (x0 t1));
+      [ let x0 := fresh in
+        intro x0;
+          simpl in *;
+          let GL0 := lazymatch goal with |- ?GL0 = _ => constr:(GL0) end in
+              let GL0' := fresh in
+              let GL1' := fresh in
+              set (GL0' := GL0);
+
+                let arg := match GL0 with appcontext[x0 ?arg] => constr:(arg) end in
+                assert (t1 = arg) by (subst t1; reflexivity); subst t1;
+                pattern (x0 arg) in GL0';
+                match goal with
+                  | [ GL0'' := ?GR _ |- _ ] => constr_eq GL0' GL0'';
+                                              pose GR as GL1'
+                end;
+
+                pattern x0 in GL1';
+                match goal with
+                  | [ GL1'' := ?GR _ |- _ ] => constr_eq GL1' GL1'';
+                                              assert (t0 = GR)
+                end;
+                subst t0; [ reflexivity | reflexivity ]
+            | clear dummy ];
+      let p := fresh in
+      pose (@path_forall_recr_beta H X T t1 t0) as p;
+        simpl in *;
+        rewrite p;
+        subst t0 t1 p.
+      rewrite transport_path_prod'_beta'.
+      (* Anomaly: Uncaught exception Invalid_argument("to_constraints: non-trivial algebraic constraint between universes", _).
+Please report. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_059.v b/test-suite/bugs/closed/HoTT_coq_059.v
new file mode 100644
index 000000000..9c7e394dc
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_059.v
@@ -0,0 +1,17 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+Set Universe Polymorphism.
+
+Inductive eq {A} (x : A) : A -> Type := eq_refl : eq x x.
+Notation "a = b" := (eq a b) : type_scope.
+
+Section foo.
+  Class Funext := { path_forall :> forall A P (f g : forall x : A, P x), (forall x, f x = g x) -> f = g }.
+  Context `{Funext, Funext}.
+
+  Set Printing Universes.
+
+  (** Typeclass resolution should pick up the different instances of Funext automatically *)
+  Definition foo := (@path_forall _ _ _ (@path_forall _ Set)).
+  (* Toplevel input, characters 0-60:
+Error: Universe inconsistency (cannot enforce Top.24 <= Top.23 because Top.23
+< Top.22 <= Top.24). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_067.v b/test-suite/bugs/closed/HoTT_coq_067.v
new file mode 100644
index 000000000..ad32a60c6
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_067.v
@@ -0,0 +1,28 @@
+Set Universe Polymorphism.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Goal forall (A : Type) (P : forall _ : A, Type) (x0 : A)
+     (p : P x0) (q : @paths (@sigT A P) (@existT A P x0 p) (@existT A P x0 p)),
+   @paths (@paths (@sigT A P) (@existT A P x0 p) (@existT A P x0 p))
+     (@idpath (@sigT A P) (@existT A P x0 p))
+     (@idpath (@sigT A P) (@existT A P x0 p)).
+  intros.
+  induction q.
+  admit.
+Qed.
+(** Error: Illegal application:
+The term "paths_rect" of type
+ "forall (A : Type) (a : A) (P : forall a0 : A, paths a a0 -> Type),
+  P a (idpath a) -> forall (y : A) (p : paths a y), P y p"
+cannot be applied to the terms
+ "{x : _ & P x}" : "Type"
+ "s" : "{x : _ & P x}"
+ "fun (a : {x : _ & P x}) (_ : paths s a) => paths (idpath a) (idpath a)"
+   : "forall a : {x : _ & P x}, paths s a -> Type"
+ "match proof_admitted return (paths (idpath s) (idpath s)) with
+  end" : "paths (idpath s) (idpath s)"
+ "s" : "{x : _ & P x}"
+ "q" : "paths (existT P x0 p) (existT P x0 p)"
+The 3rd term has type "forall a : {x : _ & P x}, paths s a -> Type"
+which should be coercible to "forall a : {x : _ & P x}, paths s a -> Type". *)
diff --git a/test-suite/bugs/closed/HoTT_coq_068.v b/test-suite/bugs/closed/HoTT_coq_068.v
new file mode 100644
index 000000000..f1cdcbf22
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_068.v
@@ -0,0 +1,61 @@
+Generalizable All Variables.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Module success.
+  Axiom bar : nat -> Type -> Type.
+
+  Definition foo (n : nat) (A : Type) : Type :=
+    match n with
+      | O => A
+      | S n' => forall x y : A, bar n' (x = y)
+    end.
+
+  Definition foo_succ n A : foo (S n) A.
+  Admitted.
+
+  Goal forall n (X Y : Type) (y : X) (x : X), bar n (x = y).
+  intros.
+  apply (foo_succ _ _).
+  Defined.
+End success.
+
+Module failure.
+  Fixpoint bar (n : nat) (A : Type) : Type :=
+    match n with
+      | O => A
+      | S n' => forall x y : A, bar n' (x = y)
+    end.
+
+  Definition foo_succ n A : bar (S n) A.
+  Admitted.
+
+  Goal forall n (X Y : Type) (y : X) (x : X), bar n (x = y).
+  intros.
+  apply foo_succ.
+  (* Toplevel input, characters 22-34:
+Error: In environment
+n : nat
+X : Type
+Y : Type
+y : X
+x : X
+Unable to unify
+ "forall x0 y0 : ?16,
+  (fix bar (n : nat) (A : Type) {struct n} : Type :=
+     match n with
+     | 0 => A
+     | S n' => forall x y : A, bar n' (x = y)
+     end) ?15 (x0 = y0)" with
+ "(fix bar (n : nat) (A : Type) {struct n} : Type :=
+     match n with
+     | 0 => A
+     | S n' => forall x y : A, bar n' (x = y)
+     end) n (x = y)".
+*)
+  Defined.
+End failure.
diff --git a/test-suite/bugs/closed/HoTT_coq_071.v b/test-suite/bugs/closed/HoTT_coq_071.v
new file mode 100644
index 000000000..b5a5ec1bd
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_071.v
@@ -0,0 +1,9 @@
+Set Universe Polymorphism.
+Definition foo : True.
+  abstract exact I.
+Defined.
+Eval hnf in foo. (* Should not be [I] *)
+Goal True.
+Proof.
+  Fail unify foo I.
+Abort.
diff --git a/test-suite/bugs/closed/HoTT_coq_079.v b/test-suite/bugs/closed/HoTT_coq_079.v
new file mode 100644
index 000000000..e70de9ca9
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_079.v
@@ -0,0 +1,16 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Inductive paths A (x : A) : A -> Type := idpath : paths x x.
+
+Notation "x = y :> A" := (@paths A x y).
+Notation "x = y" := (x = y :> _).
+
+Record foo := { x : Type; H : x = x }.
+
+Create HintDb bar discriminated.
+Hint Resolve H : bar.
+Goal forall y : foo, @x y = @x y.
+intro y.
+progress auto with bar. (* failed to progress *)
diff --git a/test-suite/bugs/closed/HoTT_coq_087.v b/test-suite/bugs/closed/HoTT_coq_087.v
new file mode 100644
index 000000000..265310b1a
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_087.v
@@ -0,0 +1,14 @@
+Structure type : Type := Pack { ob : Type }.
+Polymorphic Record category := { foo : Type }.
+Definition FuncComp := Pack category.
+Axiom C : category.
+
+Check (C : ob FuncComp). (* OK *)
+
+Canonical Structure FuncComp.
+
+Check (C : ob FuncComp).
+(* Toplevel input, characters 15-39:
+Error:
+The term "C" has type "category" while it is expected to have type
+ "ob FuncComp". *)
diff --git a/test-suite/bugs/closed/HoTT_coq_088.v b/test-suite/bugs/closed/HoTT_coq_088.v
new file mode 100644
index 000000000..b3e1df579
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_088.v
@@ -0,0 +1,78 @@
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Arguments paths_ind [A] a P f y p.
+Arguments paths_rec [A] a P f y p.
+Arguments paths_rect [A] a P f y p.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+(** A typeclass that includes the data making [f] into an adjoint equivalence. *)
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : Sect equiv_inv f;
+  eissect : Sect f equiv_inv;
+  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+}.
+
+Record Equiv A B := BuildEquiv {
+  equiv_fun :> A -> B ;
+  equiv_isequiv :> IsEquiv equiv_fun
+}.
+
+
+Definition equiv_path (A B : Type) (p : A = B) : Equiv A B.
+Admitted.
+
+Class Univalence := {
+  isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B)
+}.
+
+Definition ua_downward_closed `{Univalence} : Univalence.
+  constructor.
+  intros A B.
+  destruct H as [H].
+  generalize (fun A B => @eisretr _ _ _ (H (A : Type) (B : Type))).
+  generalize (fun A B => @eissect _ _ _ (H (A : Type) (B : Type))).
+  let g := match goal with |- _ -> _ -> ?g => constr:(g) end in
+  let U0 := match goal with |- (forall (A : ?U0) (B : ?U1), Sect (@?f A B) _) -> (forall (A : ?U2) (B : ?U3), Sect _ (@?f' A B)) -> ?g => constr:(U0) end in
+  let U1 := match goal with |- (forall (A : ?U0) (B : ?U1), Sect (@?f A B) _) -> (forall (A : ?U2) (B : ?U3), Sect _ (@?f' A B)) -> ?g => constr:(U1) end in
+  let U2 := match goal with |- (forall (A : ?U0) (B : ?U1), Sect (@?f A B) _) -> (forall (A : ?U2) (B : ?U3), Sect _ (@?f' A B)) -> ?g => constr:(U2) end in
+  let U3 := match goal with |- (forall (A : ?U0) (B : ?U1), Sect (@?f A B) _) -> (forall (A : ?U2) (B : ?U3), Sect _ (@?f' A B)) -> ?g => constr:(U3) end in
+  let f0 := match goal with |- (forall (A : ?U0) (B : ?U1), Sect (@?f A B) _) -> (forall (A : ?U2) (B : ?U3), Sect _ (@?f' A B)) -> ?g => constr:(f) end in
+  let f' := match goal with |- (forall (A : ?U0) (B : ?U1), Sect (@?f A B) _) -> (forall (A : ?U2) (B : ?U3), Sect _ (@?f' A B)) -> ?g => constr:(f') end in
+  change ((forall (A : U0) (B : U1), Sect (f0 A B) ((fun (A : U0) (B : U1) => @equiv_inv _ _ _ (H A B)) A B))
+          -> (forall (A : U2) (B : U3), Sect ((fun (A : U0) (B : U1) => @equiv_inv _ _ _ (H A B)) A B) (f' A B))
+          -> g);
+    generalize (fun (A : U0) (B : U1) => @equiv_inv _ _ _ (H A B));
+    clear H;
+    simpl;
+    intros fi sect retr.
+  pose proof fi as fi'.
+  Set Printing All.
+  change (forall (A : Type) (B : Type) (_ : Equiv A B), @paths Type A B) in fi'.
+  (*refine (@isequiv_adjointify
+              _ _
+              _ _
+              _
+              _);
+    admit.
+  Grab Existential Variables.*)
+  admit.
+  (*destruct p.*)
+  (*specialize (H (A' : Type)).*)
+Defined.
+(* Error: Unsatisfied constraints:
+Top.62 < Top.61
+Top.64 <= Top.62
+Top.63 <= Top.62
+ (maybe a bugged tactic).*)
diff --git a/test-suite/bugs/closed/HoTT_coq_090.v b/test-suite/bugs/closed/HoTT_coq_090.v
new file mode 100644
index 000000000..5c7041471
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_090.v
@@ -0,0 +1,187 @@
+(** I'm not sure if this tests what I want it to test... *)
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Notation idmap := (fun x => x).
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Arguments paths_ind [A] a P f y p.
+Arguments paths_rec [A] a P f y p.
+Arguments paths_rect [A] a P f y p.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+(** A typeclass that includes the data making [f] into an adjoint equivalence. *)
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : Sect equiv_inv f;
+  eissect : Sect f equiv_inv;
+  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+}.
+
+Arguments eisretr {A B} f {_} _.
+Arguments eissect {A B} f {_} _.
+Arguments eisadj {A B} f {_} _.
+
+
+Record Equiv A B := BuildEquiv {
+  equiv_fun :> A -> B ;
+  equiv_isequiv :> IsEquiv equiv_fun
+}.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+
+(** See above for the meaning of [simpl nomatch]. *)
+Arguments concat {A x y z} p q : simpl nomatch.
+
+(** The inverse of a path. *)
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+(** Declaring this as [simpl nomatch] prevents the tactic [simpl] from expanding it out into [match] statements.  We only want [inverse] to simplify when applied to an identity path. *)
+Arguments inverse {A x y} p : simpl nomatch.
+
+(** Note that you can use the built-in Coq tactics [reflexivity] and [transitivity] when working with paths, but not [symmetry], because it is too smart for its own good.  Instead, you can write [apply symmetry] or [eapply symmetry]. *)
+
+(** The identity path. *)
+Notation "1" := idpath : path_scope.
+
+(** The composition of two paths. *)
+Notation "p @ q" := (concat p q) (at level 20) : path_scope.
+
+(** The inverse of a path. *)
+Notation "p ^" := (inverse p) (at level 3) : path_scope.
+
+(** An alternative notation which puts each path on its own line.  Useful as a temporary device during proofs of equalities between very long composites; to turn it on inside a section, say [Open Scope long_path_scope]. *)
+Notation "p @' q" := (concat p q) (at level 21, left associativity,
+  format "'[v' p '/' '@''  q ']'") : long_path_scope.
+
+
+(** An important instance of [paths_rect] is that given any dependent type, one can _transport_ elements of instances of the type along equalities in the base.
+
+   [transport P p u] transports [u : P x] to [P y] along [p : x = y]. *)
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+
+(** See above for the meaning of [simpl nomatch]. *)
+Arguments transport {A} P {x y} p%path_scope u : simpl nomatch.
+
+
+
+Instance isequiv_path {A B : Type} (p : A = B)
+  : IsEquiv (transport (fun X:Type => X) p) | 0.
+Proof.
+  refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _);
+  admit.
+Defined.
+
+Definition equiv_path (A B : Type) (p : A = B) : Equiv A B
+  := @BuildEquiv _ _ (transport (fun X:Type => X) p) _.
+
+Arguments equiv_path : clear implicits.
+
+Definition equiv_adjointify A B (f : A -> B) (g : B -> A) (r : Sect g f) (s : Sect f g) : Equiv A B.
+Proof.
+  refine (@BuildEquiv A B f (@BuildIsEquiv A B f g r s _)).
+  admit.
+Defined.
+
+
+Set Printing Universes.
+
+Definition lift_id_type : Type.
+Proof.
+  let U0 := constr:(Type) in
+  let U1 := constr:(Type) in
+  let unif := constr:(U0 : U1) in
+  exact (forall (A : Type) (B : Type), @paths U0 A B -> @paths U1 A B).
+Defined.
+
+Definition lower_id_type : Type.
+Proof.
+  let U0 := constr:(Type) in
+  let U1 := constr:(Type) in
+  let unif := constr:(U0 : U1) in
+  exact ((forall (A : Type) (B : Type), IsEquiv (equiv_path (A : U0) (B : U0)))
+         -> forall (A : Type) (B : Type),  @paths U1 A B -> @paths U0 A B).
+Defined.
+
+Definition lift_id : lift_id_type :=
+  fun A B p => match p in @paths _ _ B return @paths Type (A : Type) (B : Type) with
+                 | idpath => idpath
+               end.
+
+Definition lower_id : lower_id_type.
+Proof.
+  intros ua A B p.
+  specialize (ua A B).
+  apply (@equiv_inv _ _ (equiv_path A B) _).
+  simpl.
+  pose (f := transport idmap p : A -> B).
+  pose (g := transport idmap p^ : B -> A).
+  refine (@equiv_adjointify
+            _ _
+            f g
+            _ _);
+    subst f g; unfold transport, inverse;
+    clear ua;
+    [ intro x
+    | exact match p as p in (_ = B) return
+                  (forall x : (A : Type),
+                     @paths (* Top.904 *)
+                       A
+                       match
+                         match
+                           p in (paths _ a)
+                           return (@paths (* Top.906 *) Type (* Top.900 *) a A)
+                         with
+                           | idpath => @idpath (* Top.906 *) Type (* Top.900 *) A
+                         end in (paths _ a) return a
+                       with
+                         | idpath => match p in (paths _ a) return a with
+                                       | idpath => x
+                                     end
+                       end x)
+            with
+              | idpath => fun _ => idpath
+            end ].
+
+  - pose proof (match p as p in (_ = B) return
+                      (forall x : (B : Type),
+                         match p in (_ = a) return (a : Type) with
+                           | idpath =>
+                             match
+                               match p in (_ = a) return (@paths Type (a : Type) (A : Type)) with
+                                 | idpath => idpath
+                               end in (_ = a) return (a : Type)
+                             with
+                               | idpath => x
+                             end
+                         end = x)
+                with
+                  | idpath => fun _ => idpath
+                end x) as p'.
+    admit.
+Defined.
+(* Error: Illegal application:
+The term "paths (* Top.96 *)" of type
+ "forall A : Type (* Top.96 *), A -> A -> Type (* Top.96 *)"
+cannot be applied to the terms
+ "Type (* Top.100 *)" : "Type (* Top.100+1 *)"
+ "a" : "Type (* Top.60 *)"
+ "A" : "Type (* Top.57 *)"
+The 2nd term has type "Type (* Top.60 *)" which should be coercible to
+ "Type (* Top.100 *)".
+ *)
diff --git a/test-suite/bugs/closed/HoTT_coq_091.v b/test-suite/bugs/closed/HoTT_coq_091.v
new file mode 100644
index 000000000..1e4497e75
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_091.v
@@ -0,0 +1,191 @@
+Set Implicit Arguments.
+
+Set Printing Universes.
+
+Set Asymmetric Patterns.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Arguments paths_ind [A] a P f y p.
+Arguments paths_rec [A] a P f y p.
+Arguments paths_rect [A] a P f y p.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+Arguments ap {A B} f {x y} p : simpl nomatch.
+
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+
+(** A typeclass that includes the data making [f] into an adjoint equivalence. *)
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : Sect equiv_inv f;
+  eissect : Sect f equiv_inv;
+  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+}.
+
+Arguments eisretr {A B} f {_} _.
+Arguments eissect {A B} f {_} _.
+Arguments eisadj {A B} f {_} _.
+
+
+Inductive type_eq (A : Type) : Type -> Type :=
+| type_eq_refl : type_eq A A
+| type_eq_impossible : False -> forall B : Type, type_eq A B.
+
+Definition type_eq_sym {A B} (p : type_eq A B) : type_eq B A
+  := match p in (type_eq _ B) return (type_eq B A) with
+       | type_eq_refl => type_eq_refl _
+       | type_eq_impossible f B => type_eq_impossible _ f A
+     end.
+
+Definition type_eq_sym_type_eq_sym {A B} (p : type_eq A B) : type_eq_sym (type_eq_sym p) = p
+  := match p as p return type_eq_sym (type_eq_sym p) = p with
+       | type_eq_refl => idpath
+       | type_eq_impossible f _ => idpath
+     end.
+
+Module Type LiftT.
+  Section local.
+    Let type_cast_up_type : Type.
+    Proof.
+      let U0 := constr:(Type) in
+      let U1 := constr:(Type) in
+      let unif := constr:(U0 : U1) in
+      exact (forall T : U0, { T' : U1 & type_eq T' T }).
+    Defined.
+
+    Axiom type_cast_up : type_cast_up_type.
+  End local.
+
+  Definition Lift (T : Type) := projT1 (type_cast_up T).
+  Definition lift {T} : T -> Lift T
+    := match projT2 (type_cast_up T) in (type_eq _ T') return T' -> Lift T with
+         | type_eq_refl => fun x => x
+         | type_eq_impossible bad _ => match bad with end
+       end.
+  Section equiv.
+    Definition lower' {T} : Lift T -> T
+      := match projT2 (type_cast_up T) in (type_eq _ T') return Lift T -> T' with
+           | type_eq_refl => fun x => x
+           | type_eq_impossible bad _ => match bad with end
+         end.
+    Definition lift_lower {T} (x : Lift T) : lift (lower' x) = x.
+    Proof.
+      unfold lower', lift.
+      destruct (projT2 (type_cast_up T)) as [|[]].
+      reflexivity.
+    Defined.
+    Definition lower_lift {T} (x : T) : lower' (lift x) = x.
+    Proof.
+      unfold lower', lift, Lift in *.
+      destruct (type_cast_up T) as [T' p]; simpl.
+      let y := match goal with |- ?y => constr:(y) end in
+      let P := match (eval pattern p in y) with ?f p => constr:(f) end in
+      apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *.
+      generalize (type_eq_sym p); intro p'; clear p.
+      destruct p' as [|[]]; simpl.
+      reflexivity.
+    Defined.
+
+    Global Instance isequiv_lift A : IsEquiv (@lift A).
+    Proof.
+      refine (@BuildIsEquiv
+                _ _
+                lift lower'
+                lift_lower
+                lower_lift
+                _).
+      compute.
+      intro x.
+      destruct (type_cast_up A) as [T' p].
+      let y := match goal with |- ?y => constr:(y) end in
+      let P := match (eval pattern p in y) with ?f p => constr:(f) end in
+      apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *.
+      generalize (type_eq_sym p); intro p'; clear p.
+      destruct p' as [|[]]; simpl.
+      reflexivity.
+    Defined.
+  End equiv.
+  Definition lower {A} := (@equiv_inv _ _ (@lift A) _).
+End LiftT.
+
+Module Lift : LiftT.
+  Section local.
+    Let type_cast_up_type : Type.
+    Proof.
+      let U0 := constr:(Type) in
+      let U1 := constr:(Type) in
+      let unif := constr:(U0 : U1) in
+      exact (forall T : U0, { T' : U1 & type_eq T' T }).
+    Defined.
+
+    Definition type_cast_up : type_cast_up_type
+      := fun T => existT (fun T' => type_eq T' T) T (type_eq_refl _).
+  End local.
+
+  Definition Lift (T : Type) := projT1 (type_cast_up T).
+  Definition lift {T} : T -> Lift T
+    := match projT2 (type_cast_up T) in (type_eq _ T') return T' -> Lift T with
+         | type_eq_refl => fun x => x
+         | type_eq_impossible bad _ => match bad with end
+       end.
+  Section equiv.
+    Definition lower' {T} : Lift T -> T
+      := match projT2 (type_cast_up T) in (type_eq _ T') return Lift T -> T' with
+           | type_eq_refl => fun x => x
+           | type_eq_impossible bad _ => match bad with end
+         end.
+    Definition lift_lower {T} (x : Lift T) : lift (lower' x) = x.
+    Proof.
+      unfold lower', lift.
+      destruct (projT2 (type_cast_up T)) as [|[]].
+      reflexivity.
+    Defined.
+    Definition lower_lift {T} (x : T) : lower' (lift x) = x.
+    Proof.
+      unfold lower', lift, Lift in *.
+      destruct (type_cast_up T) as [T' p]; simpl.
+      let y := match goal with |- ?y => constr:(y) end in
+      let P := match (eval pattern p in y) with ?f p => constr:(f) end in
+      apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *.
+      generalize (type_eq_sym p); intro p'; clear p.
+      destruct p' as [|[]]; simpl.
+      reflexivity.
+    Defined.
+
+
+    Global Instance isequiv_lift A : IsEquiv (@lift A).
+    Proof.
+      refine (@BuildIsEquiv
+                _ _
+                lift lower'
+                lift_lower
+                lower_lift
+                _).
+      compute.
+      intro x.
+      destruct (type_cast_up A) as [T' p].
+      let y := match goal with |- ?y => constr:(y) end in
+      let P := match (eval pattern p in y) with ?f p => constr:(f) end in
+      apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *.
+      generalize (type_eq_sym p); intro p'; clear p.
+      destruct p' as [|[]]; simpl.
+      reflexivity.
+    Defined.
+  End equiv.
+  Definition lower {A} := (@equiv_inv _ _ (@lift A) _).
+End Lift.
+(* Toplevel input, characters 15-24:
+Anomaly: Invalid argument: enforce_eq_instances called with instances of different lengths.
+Please report. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_094.v b/test-suite/bugs/closed/HoTT_coq_094.v
new file mode 100644
index 000000000..13e0605dc
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_094.v
@@ -0,0 +1,9 @@
+Record PreCategory :=  Build_PreCategory' { object :> Type }.
+Class Foo (X : Type) := {}.
+Class Bar := {}.
+Definition functor_category `{Bar} (C D : PreCategory)  `{Foo (object D)} : PreCategory.
+Admitted.
+Fail Definition functor_object_of `{Bar} (C1 C2 D : PreCategory) `{Foo (object D)}
+: functor_category C1 (functor_category C2 D) -> True.
+(** Anomaly: File "toplevel/himsg.ml", line ..., characters ...: Assertion failed.
+Please report. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_097.v b/test-suite/bugs/closed/HoTT_coq_097.v
new file mode 100644
index 000000000..38e8007b6
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_097.v
@@ -0,0 +1,5 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+Set Universe Polymorphism.
+Set Printing Universes.
+Inductive Empty : Set := .
+(* Error: Universe inconsistency. Cannot enforce Prop <= Set). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_099.v b/test-suite/bugs/closed/HoTT_coq_099.v
new file mode 100644
index 000000000..9b6ace824
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_099.v
@@ -0,0 +1,61 @@
+(* File reduced by coq-bug-finder from 138 lines to 78 lines. *)
+Set Implicit Arguments.
+Generalizable All Variables.
+Set Universe Polymorphism.
+Delimit Scope object_scope with object.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Record Category (obj : Type) :=
+  {
+    Object :> _ := obj;
+    Morphism : obj -> obj -> Type;
+
+    Identity : forall x, Morphism x x;
+    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+  }.
+
+Arguments Identity {obj%type} [!C%category] x%object : rename.
+Arguments Compose {obj%type} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
+Bind Scope category_scope with Category.
+
+Record Functor `(C : @Category objC) `(D : @Category objD)
+  := { ObjectOf :> objC -> objD;
+       MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d) }.
+
+Record NaturalTransformation `(C : @Category objC) `(D : @Category objD) (F G : Functor C D)
+  := { ComponentsOf :> forall c, D.(Morphism) (F c) (G c) }.
+
+Definition ProductCategory `(C : @Category objC) `(D : @Category objD)
+: @Category (objC * objD)%type
+  := @Build_Category _
+                     (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type)
+                     (fun o => (Identity (fst o), Identity (snd o)))
+                     (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1))).
+
+Infix "*" := ProductCategory : category_scope.
+
+Record IsomorphismOf `{C : @Category objC} {s d} (m : C.(Morphism) s d) :=
+  { IsomorphismOf_Morphism :> C.(Morphism) s d := m;
+    Inverse : C.(Morphism) d s }.
+
+Record NaturalIsomorphism `(C : @Category objC) `(D : @Category objD) (F G : Functor C D)
+  := { NaturalIsomorphism_Transformation :> NaturalTransformation F G;
+       NaturalIsomorphism_Isomorphism : forall x : objC, IsomorphismOf (NaturalIsomorphism_Transformation x) }.
+
+Section PreMonoidalCategory.
+  Context `(C : @Category objC).
+  Definition TriMonoidalProductL : Functor (C * C * C) C.
+    admit.
+  Defined.
+  Definition TriMonoidalProductR : Functor (C * C * C) C.
+    admit.
+  Defined. (** Replacing [admit. Defined.] with [Admitted.] satisfies the constraints *)
+  Variable Associator : NaturalIsomorphism TriMonoidalProductL TriMonoidalProductR.
+  (* Toplevel input, characters 15-96:
+Error: Unsatisfied constraints:
+Coq.Init.Datatypes.28 <= Coq.Init.Datatypes.29
+Top.168 <= Coq.Init.Datatypes.29
+Top.168 <= Coq.Init.Datatypes.28
+Top.169 <= Coq.Init.Datatypes.29
+Top.169 <= Coq.Init.Datatypes.28
+ (maybe a bugged tactic). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_100.v b/test-suite/bugs/closed/HoTT_coq_100.v
new file mode 100644
index 000000000..c39b70934
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_100.v
@@ -0,0 +1,151 @@
+(* File reduced by coq-bug-finder from 335 lines to 115 lines. *)
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Generalizable All Variables.
+Record Category (obj : Type) :=
+  Build_Category {
+      Object :> _ := obj;
+      Morphism : obj -> obj -> Type;
+
+      Identity : forall x, Morphism x x;
+      Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+    }.
+
+Arguments Identity {obj%type} [!C] x : rename.
+
+Arguments Compose {obj%type} [!C s d d'] m1 m2 : rename.
+Record > Category' :=
+  {
+    LSObject : Type;
+
+    LSUnderlyingCategory :> @Category LSObject
+  }.
+
+Section Functor.
+
+  Context `(C : @Category objC).
+  Context `(D : @Category objD).
+  Record Functor :=
+    {
+      ObjectOf :> objC -> objD;
+      MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
+    }.
+
+End Functor.
+Section FunctorComposition.
+
+  Context `(C : @Category objC).
+  Context `(D : @Category objD).
+  Context `(E : @Category objE).
+  Definition ComposeFunctors (G : Functor D E) (F : Functor C D) : Functor C E.
+
+  Admitted.
+End FunctorComposition.
+Section IdentityFunctor.
+
+  Context `(C : @Category objC).
+  Definition IdentityFunctor : Functor C C.
+
+    admit.
+  Defined.
+End IdentityFunctor.
+Section ProductCategory.
+
+  Context `(C : @Category objC).
+  Context `(D : @Category objD).
+  Definition ProductCategory : @Category (objC * objD)%type.
+
+    refine (@Build_Category _
+                            (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type)
+                            (fun o => (Identity (fst o), Identity (snd o)))
+                            (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1)))).
+  Defined.
+End ProductCategory.
+Parameter TerminalCategory : Category unit.
+
+Section ComputableCategory.
+
+  Variable I : Type.
+  Variable Index2Object : I -> Type.
+  Variable Index2Cat : forall i : I, @Category (@Index2Object i).
+  Local Coercion Index2Cat : I >-> Category.
+
+  Definition ComputableCategory : @Category I.
+
+    refine (@Build_Category _
+                            (fun C D : I => Functor C D)
+                            (fun o : I => IdentityFunctor o)
+                            (fun C D E : I => ComposeFunctors (C := C) (D := D) (E := E))).
+  Defined.
+End ComputableCategory.
+Definition LocallySmallCat := ComputableCategory _ LSUnderlyingCategory.
+Section CommaCategory.
+
+  Context `(A : @Category objA).
+  Context `(B : @Category objB).
+  Context `(C : @Category objC).
+  Variable S : Functor A C.
+  Variable T : Functor B C.
+  Record CommaCategory_Object := { CommaCategory_Object_Member :> { ab : objA * objB & C.(Morphism) (S (fst ab)) (T (snd ab)) } }.
+
+End CommaCategory.
+Definition SliceCategory_Functor `(C : @Category objC) (a : C) : Functor TerminalCategory C
+  := {| ObjectOf := (fun _ => a);
+        MorphismOf := (fun _ _ _ => Identity a)
+     |}.
+
+Definition SliceCategoryOver
+: forall (objC : Type) (C : Category objC) (a : C),
+    Category
+      (CommaCategory_Object (IdentityFunctor C)
+                            (SliceCategory_Functor C a)).
+
+  admit.
+Defined.
+Section CommaCategoryProjectionFunctor.
+
+  Context `(A : Category objA).
+  Context `(B : Category objB).
+  Let X : LocallySmallCat.
+
+  Proof.
+    hnf.
+    pose (@SliceCategoryOver _ LocallySmallCat).
+    exact (ProductCategory A B).
+    Set Printing Universes.
+  Defined.
+(* Error: Illegal application:
+The term
+ "CommaCategory_Object (* Top.306 Top.307 Top.305 Top.300 Top.305 Top.306 *)"
+of type
+ "forall (objA : Type (* Top.305 *))
+    (A : Category (* Top.306 Top.305 *) objA) (objB : Type (* Top.307 *))
+    (B : Category (* Top.300 Top.307 *) objB) (objC : Type (* Top.305 *))
+    (C : Category (* Top.306 Top.305 *) objC),
+  Functor (* Top.306 Top.305 Top.305 Top.306 *) A C ->
+  Functor (* Top.300 Top.307 Top.305 Top.306 *) B C ->
+  Type (* max(Top.307, Top.305, Top.306) *)"
+cannot be applied to the terms
+ "Category' (* Top.312 Top.311 *)" : "Type (* max(Top.311+1, Top.312+1) *)"
+ "LocallySmallCat (* Top.309 Top.310 Top.311 Top.312 Top.313 Top.314 Top.306 Top.316 Top.305 *)"
+   : "Category (* Top.306 Top.305 *) Category' (* Top.312 Top.311 *)"
+ "unit" : "Set"
+ "TerminalCategory (* Top.300 *)" : "Category (* Top.300 Set *) unit"
+ "Category' (* Top.312 Top.311 *)" : "Type (* max(Top.311+1, Top.312+1) *)"
+ "LocallySmallCat (* Top.309 Top.310 Top.311 Top.312 Top.313 Top.314 Top.306 Top.316 Top.305 *)"
+   : "Category (* Top.306 Top.305 *) Category' (* Top.312 Top.311 *)"
+ "IdentityFunctor (* Top.299 Top.302 Top.301 Top.305 Top.306 *)
+    LocallySmallCat (* Top.309 Top.310 Top.311 Top.312 Top.313 Top.314
+    Top.306 Top.316 Top.305 *)"
+   : "Functor (* Top.306 Top.305 Top.305 Top.306 *) LocallySmallCat
+        (* Top.309 Top.310 Top.311 Top.312 Top.313 Top.314 Top.306 Top.316
+        Top.305 *) LocallySmallCat (* Top.309 Top.310 Top.311 Top.312 Top.313
+        Top.314 Top.306 Top.316 Top.305 *)"
+ "SliceCategory_Functor (* Top.305 Top.306 Top.307 Top.300 *) LocallySmallCat
+    (* Top.309 Top.310 Top.311 Top.312 Top.313 Top.314 Top.306 Top.316
+    Top.305 *) a"
+   : "Functor (* Top.300 Top.307 Top.305 Top.306 *) TerminalCategory
+        (* Top.300 *) LocallySmallCat (* Top.309 Top.310 Top.311 Top.312
+        Top.313 Top.314 Top.306 Top.316 Top.305 *)"
+The 4th term has type "Category (* Top.300 Set *) unit"
+which should be coercible to "Category (* Top.300 Top.307 *) unit". *)
diff --git a/test-suite/bugs/closed/HoTT_coq_108.v b/test-suite/bugs/closed/HoTT_coq_108.v
new file mode 100644
index 000000000..77f921b7c
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_108.v
@@ -0,0 +1,127 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* NOTE: This bug is only triggered with -load-vernac-source / in interactive mode. *)
+(* File reduced by coq-bug-finder from 139 lines to 124 lines. *)
+Set Universe Polymorphism.
+Reserved Notation "g 'o' f" (at level 40, left associativity).
+Generalizable All Variables.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
+: forall x, f x = g x
+  := fun x => match h with idpath => idpath end.
+
+Definition ap11 {A B} {f g:A->B} (h:f=g) {x y:A} (p:x=y) : f x = g y.
+  admit.
+Defined.
+Class IsEquiv {A B : Type} (f : A -> B) := {}.
+Class Contr_internal (A : Type) := BuildContr {
+                                       center : A ;
+                                       contr : (forall y : A, center = y)
+                                     }.
+
+Arguments center A {_}.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+
+Fixpoint nat_to_trunc_index (n : nat) : trunc_index
+  := match n with
+       | 0 => trunc_S (trunc_S minus_two)
+       | S n' => trunc_S (nat_to_trunc_index n')
+     end.
+
+Coercion nat_to_trunc_index : nat >-> trunc_index.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | minus_two => Contr_internal A
+    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+Class IsTrunc (n : trunc_index) (A : Type) : Type :=
+  Trunc_is_trunc : IsTrunc_internal n A.
+
+Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A)
+: IsTrunc n (x = y)
+  := H x y.
+
+Notation Contr := (IsTrunc minus_two).
+
+Notation IsHSet := (IsTrunc 0).
+
+Class Funext :=
+  { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+Global Instance contr_forall `{Funext} `{P : A -> Type} `{forall a, Contr (P a)}
+: Contr (forall a, P a) | 100.
+admit.
+Defined.
+Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
+Global Instance trunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)}
+: IsTrunc n (forall a, P a) | 100.
+Proof.
+  generalize dependent P.
+  induction n as [ | n' IH]; [ | admit ]; simpl; intros P ?.
+                                                        exact _.
+Defined.
+Set Implicit Arguments.
+
+Record PreCategory :=
+  { object :> Type;
+    morphism : object -> object -> Type;
+    identity : forall x, morphism x x;
+    compose : forall s d d', morphism d d' -> morphism s d -> morphism s d';
+    trunc_morphism : forall s d, IsHSet (morphism s d) }.
+
+Existing Instance trunc_morphism.
+Infix "o" := (@compose _ _ _ _) : morphism_scope.
+Local Open Scope morphism_scope.
+
+Record Functor (C D : PreCategory) :=
+  { object_of :> C -> D;
+    morphism_of : forall s d, morphism C s d
+                              -> morphism D (object_of s) (object_of d);
+    composition_of : forall s d d'
+                            (m1 : morphism C s d) (m2: morphism C d d'),
+                       morphism_of _ _ (m2 o m1)
+                       = (morphism_of _ _ m2) o (morphism_of _ _ m1);
+    identity_of : forall x, morphism_of _ _ (@identity _ x)
+                            = @identity _ (object_of x) }.
+
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+
+Section path_functor.
+  Context `{Funext}.
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+  Local Notation path_functor'_T F G
+    := { HO : object_of F = object_of G
+       | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) (GO d))
+                   HO
+                   (morphism_of F)
+         = morphism_of G }
+         (only parsing).
+  Definition path_functor'_sig (F G : Functor C D) : path_functor'_T F G -> F = G.
+  Proof.
+    intros [H' H''].
+    destruct F, G; simpl in *.
+    induction H'; induction H''; simpl.
+    apply ap11; [ apply ap | ];
+    apply center; abstract exact _.
+    Set Printing Universes.
+    (* Fail Defined.*)
+  (* The command has indeed failed with message:
+=> Error: path_functor'_sig_subproof already exists. *)
+  Defined.
+(* Anomaly: Backtrack.backto 55: a state with no vcs_backup. Please report. *)
+End path_functor.
diff --git a/test-suite/bugs/closed/HoTT_coq_112.v b/test-suite/bugs/closed/HoTT_coq_112.v
new file mode 100644
index 000000000..150f2ecc8
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_112.v
@@ -0,0 +1,75 @@
+(* File reduced by coq-bug-finder from 4464 lines to 4137 lines, then from 3683 lines to 118 lines, then from 124 lines to 75 lines. *)
+Set Universe Polymorphism.
+Definition admit {T} : T.
+Admitted.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
+  : forall x, f x = g x
+  := fun x => match h with idpath => idpath end.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : forall x, f (equiv_inv x) = x
+}.
+
+Arguments eisretr {A B} f {_} _.
+
+Record Equiv A B := BuildEquiv {
+  equiv_fun :> A -> B ;
+  equiv_isequiv :> IsEquiv equiv_fun
+}.
+
+Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
+Local Open Scope equiv_scope.
+
+Instance isequiv_path {A B : Type} (p : A = B)
+  : IsEquiv (transport (fun X:Type => X) p) | 0
+  := admit.
+Definition equiv_path (A B : Type) (p : A = B) : A <~> B
+  := BuildEquiv _ _ (transport (fun X:Type => X) p) _.
+
+Class Univalence := {
+  isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B)
+}.
+
+Section Univalence.
+  Context `{Univalence}.
+
+  Definition path_universe_uncurried {A B : Type} (f : A <~> B) : A = B
+    := (equiv_path A B)^-1 f.
+
+  Definition path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B)
+    := path_universe_uncurried (BuildEquiv _ _ f feq).
+
+  Set Printing Universes.
+  Definition transport_path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : A)
+  : transport (fun X:Type => X) (path_universe f) z = f z
+    := apD10 (ap (equiv_fun A B) (eisretr (equiv_path A B) (BuildEquiv _ _ f feq))) z.
+  (* Toplevel input, characters 0-231:
+Error: Illegal application:
+The term "isequiv_equiv_path (* Top.1003 Top.1003 Top.1001 Top.997 *)"
+of type
+ "Univalence (* Top.1003 Top.1003 Top.1001 Top.997 *) ->
+  forall (A : Type (* Top.1003 *)) (B : Type (* Top.997 *)),
+  IsEquiv (* Top.1003 Top.1001 *)
+    (equiv_path (* Top.997 Top.1003 Top.1001 Top.1003 *) A B)"
+cannot be applied to the terms
+ "H" : "Univalence (* Top.934 Top.935 Top.936 Top.937 *)"
+ "A" : "Type (* Top.996 *)"
+ "B" : "Type (* Top.997 *)"
+The 1st term has type "Univalence (* Top.934 Top.935 Top.936 Top.937 *)"
+which should be coercible to
+ "Univalence (* Top.1003 Top.1003 Top.1001 Top.997 *)".
+ *)
diff --git a/test-suite/bugs/closed/HoTT_coq_116.v b/test-suite/bugs/closed/HoTT_coq_116.v
new file mode 100644
index 000000000..d408557d5
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_116.v
@@ -0,0 +1,13 @@
+Set Universe Polymorphism.
+Section foo.
+  Let U := Type.
+  Let U' : Type.
+  Proof.
+    let U' := constr:(Type) in
+    let U_le_U' := constr:(fun x : U => (x : U')) in
+    exact U'.
+  Defined.
+  Inductive t : U' := .
+End foo.
+(* Toplevel input, characters 15-23:
+Error: No such section variable or assumption: U'. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_117.v b/test-suite/bugs/closed/HoTT_coq_117.v
new file mode 100644
index 000000000..5fbcfef4e
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_117.v
@@ -0,0 +1,25 @@
+(* File reduced by coq-bug-finder from original input, then from 1461 lines to 81 lines, then from 84 lines to 40 lines, then from 50 lines to 24 lines *)
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Class Contr_internal (A : Type) := BuildContr {
+  center : A ;
+  contr : (forall y : A, center = y)
+}.
+Class Funext := {}.
+
+Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
+  (forall x, f x = g x) -> f = g.
+
+Admitted.
+
+Inductive Empty : Set := .
+Instance contr_from_Empty {_ : Funext} (A : Type) :
+  Contr_internal (Empty -> A) :=
+  BuildContr _
+             (Empty_rect (fun _ => A))
+             (fun f => path_forall _ f (fun x => Empty_rect _ x)).
+(* Toplevel input, characters 15-220:
+Anomaly: unknown meta ?190. Please report. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_118.v b/test-suite/bugs/closed/HoTT_coq_118.v
new file mode 100644
index 000000000..14ad0e49d
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_118.v
@@ -0,0 +1,35 @@
+(* File reduced by coq-bug-finder from original input, then from 5631 lines to 557 lines, then from 526 lines to 181 lines, then from 189 lines to 154 lines, then from 153 lines to 107 lines, then from 97 lines to 56 lines, then from 50 lines to 37 lines *)
+Generalizable All Variables.
+Set Universe Polymorphism.
+Definition admit {T} : T.
+Admitted.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y" := (@paths _ x y) : type_scope.
+Class Contr_internal (A : Type) := BuildContr { center : A }.
+Arguments center A {_}.
+Instance contr_paths_contr `{Contr_internal A} (x y : A) : Contr_internal (x = y) := admit.
+Inductive Unit : Set := tt.
+Instance contr_unit : Contr_internal Unit | 0 := admit.
+Record PreCategory := { morphism : Type }.
+Class IsIsomorphism {C : PreCategory} (m : morphism C) := { left_inverse : m = m }.
+Definition indiscrete_category : PreCategory := @Build_PreCategory Unit.
+Goal forall (X : Type) (_ : forall x y : X, Contr_internal (@paths X x y)) (s : X),
+       @IsIsomorphism indiscrete_category tt -> True.
+Proof.
+  intros X H s [p].
+  simpl in *.
+  assert (idpath = p).
+  clear.
+  assert (H : forall p : tt = tt, idpath = p) by (intro; exact (center _)).
+  clear H.
+  exact (center _).
+  (* Toplevel input, characters 15-32:
+Error:
+Unable to satisfy the following constraints:
+In environment:
+p : tt = tt
+
+?46 : "Contr_internal (idpath = p)"
+ *)
diff --git a/test-suite/bugs/closed/HoTT_coq_121.v b/test-suite/bugs/closed/HoTT_coq_121.v
new file mode 100644
index 000000000..cce288cff
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_121.v
@@ -0,0 +1,18 @@
+(* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from 351 lines to 260 lines, then from 208 lines to 162 lines, then from 167 lines to 154 lines, then from 146 lines to 72 lines, then from 82 lines to 70 lines, then from 79 lines to 49 lines, then from 59 lines to 16 lines *)
+
+Set Universe Polymorphism.
+Generalizable All Variables.
+Record hSet := BuildhSet {setT:> Type}.
+Axiom minus1Trunc : Type -> Type.
+Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT  P).
+Definition issurj {X Y} (f:X->Y) := forall y:Y, hexists (fun x => (f x) = y).
+Lemma isepi_issurj {X Y} (f:X->Y): issurj f.
+Proof.
+  intros y.
+  admit.
+Defined. (* Toplevel input, characters 15-23:
+Error: Unsatisfied constraints:
+Top.38 <= Coq.Init.Specif.7
+Top.43 <= Top.38
+Top.43 <= Coq.Init.Specif.8
+ (maybe a bugged tactic). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v
new file mode 100644
index 000000000..994dff637
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_123.v
@@ -0,0 +1,171 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") *)
+(* File reduced by coq-bug-finder from original input, then from 4988 lines to 856 lines, then from 648 lines to 398 lines, then from 401 lines to 332 lines, then from 287 lines to 250 lines, then from 257 lines to 241 lines, then from 223 lines to 175 lines *)
+Set Universe Polymorphism.
+Set Asymmetric Patterns.
+Reserved Notation "g 'o' f" (at level 40, left associativity).
+Generalizable All Variables.
+Definition admit {T} : T.
+Admitted.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y" := (@paths _ x y) : type_scope.
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) : Type
+  := forall x:A, f x = g x.
+Hint Unfold pointwise_paths : typeclass_instances.
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
+Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
+: forall x, f x = g x
+  := fun x => match h with idpath => idpath end.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }.
+
+Record Equiv A B := BuildEquiv { equiv_fun :> A -> B ; equiv_isequiv :> IsEquiv equiv_fun }.
+Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
+Class Contr_internal (A : Type) := {}.
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | minus_two => Contr_internal A
+    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+
+Class IsTrunc (n : trunc_index) (A : Type) : Type :=
+  Trunc_is_trunc : IsTrunc_internal n A.
+
+Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A)
+: IsTrunc n (x = y)
+  := H x y.
+
+Notation IsHSet := (IsTrunc minus_two).
+
+Class Funext :=
+  { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+
+Local Open Scope equiv_scope.
+
+Global Instance isequiv_inverse `{IsEquiv A B f} : IsEquiv f^-1 | 10000
+  := BuildIsEquiv B A f^-1 f.
+Instance trunc_succ `{IsTrunc n A} : IsTrunc (trunc_S n) A | 1000.
+
+admit.
+
+Defined.
+Definition trunc_equiv `(f : A -> B)
+           `{IsTrunc n A} `{IsEquiv A B f}
+: IsTrunc n B.
+  admit.
+Defined.
+Definition trunc_equiv' `(f : A <~> B) `{IsTrunc n A}
+: IsTrunc n B
+  := admit.
+Set Implicit Arguments.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope object_scope with object.
+Record PreCategory :=
+  Build_PreCategory {
+      object :> Type;
+      morphism : object -> object -> Type;
+
+      identity : forall x, morphism x x;
+      compose : forall s d d',
+                  morphism d d'
+                  -> morphism s d
+                  -> morphism s d'
+                              where "f 'o' g" := (compose f g);
+
+      associativity : forall x1 x2 x3 x4
+                             (m1 : morphism x1 x2)
+                             (m2 : morphism x2 x3)
+                             (m3 : morphism x3 x4),
+                        (m3 o m2) o m1 = m3 o (m2 o m1);
+
+      left_identity : forall a b (f : morphism a b), identity b o f = f;
+      right_identity : forall a b (f : morphism a b), f o identity a = f;
+
+      trunc_morphism : forall s d, IsHSet (morphism s d)
+    }.
+Existing Instance trunc_morphism.
+
+Infix "o" := (@compose _ _ _ _) : morphism_scope.
+Delimit Scope functor_scope with functor.
+
+Local Open Scope morphism_scope.
+Record Functor (C D : PreCategory) :=
+  {
+    object_of :> C -> D;
+    morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d)
+  }.
+
+Global Instance trunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)}
+: IsTrunc n (forall a, P a) | 100.
+Proof.
+    generalize dependent P.
+  induction n as [ | n' IH]; (simpl; intros P ?).
+  - admit.
+  - pose (fun f g => trunc_equiv (@apD10 A P f g) ^-1); admit.
+Defined.
+Instance trunc_sigma `{P : A -> Type}
+         `{IsTrunc n A} `{forall a, IsTrunc n (P a)}
+: IsTrunc n (sigT P) | 100.
+admit.
+Defined.
+Record NaturalTransformation C D (F G : Functor C D) :=
+  Build_NaturalTransformation' {
+      components_of :> forall c, morphism D (F c) (G c)
+    }.
+Section path_natural_transformation.
+  Context `{Funext}.
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+  Variables F G : Functor C D.
+  Lemma equiv_sig_natural_transformation
+  : { CO : forall x, morphism D (F x) (G x)
+    & forall s d (m : morphism C s d),
+        CO d o morphism_of F _ _ m = morphism_of G _ _ m o CO s }
+      <~> NaturalTransformation F G.
+
+    admit.
+  Defined.
+  Global Instance trunc_natural_transformation
+  : IsHSet (NaturalTransformation F G).
+  Proof.
+    eapply trunc_equiv'; [ exact equiv_sig_natural_transformation | ].
+    typeclasses eauto.
+  Qed.
+  Lemma path_natural_transformation (T U : NaturalTransformation F G)
+  : components_of T == components_of U
+    -> T = U.
+    admit.
+  Defined.
+End path_natural_transformation.
+Ltac path_natural_transformation :=
+  repeat match goal with
+           | _ => intro
+           | _ => apply path_natural_transformation; simpl
+         end.
+
+Section FunctorSectionCategory.
+  Context `{Funext}.
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+
+  Definition category_of_sections : PreCategory.
+  Proof.
+    refine (@Build_PreCategory
+              (Functor D C)
+              (fun F G => NaturalTransformation F G)
+              admit
+              admit
+              _
+              _
+              _
+              _);
+    abstract (path_natural_transformation; admit).
+  Defined. (* Stack overflow *)
diff --git a/test-suite/bugs/opened/HoTT_coq_074.v b/test-suite/bugs/opened/HoTT_coq_074.v
new file mode 100644
index 000000000..7c88447b2
--- /dev/null
+++ b/test-suite/bugs/opened/HoTT_coq_074.v
@@ -0,0 +1,12 @@
+Monomorphic Definition U1 := Type.
+Monomorphic Definition U2 := Type.
+
+Set Printing Universes.
+Definition foo : True.
+Fail let t1 := type of U1 in
+let t2 := type of U2 in
+pose (t1 : t2). (* Error:
+The term "Type (* Top.1+1 *)" has type "Type (* Top.1+2 *)"
+while it is expected to have type "Type (* Top.2+1 *)". *)
+exact I.
+Defined.
diff --git a/test-suite/bugs/opened/HoTT_coq_077.v b/test-suite/bugs/opened/HoTT_coq_077.v
new file mode 100644
index 000000000..68d305661
--- /dev/null
+++ b/test-suite/bugs/opened/HoTT_coq_077.v
@@ -0,0 +1,39 @@
+Set Implicit Arguments.
+
+Require Import Logic.
+
+Set Asymmetric Patterns.
+Set Record Elimination Schemes.
+Set Primitive Projections.
+
+Record prod (A B : Type) : Type :=
+  pair { fst : A; snd : B }.
+
+Print prod_rect.
+(** prod_rect =
+fun (A B : Type) (P : prod A B -> Type)
+  (f : forall (fst : A) (snd : B), P {| fst := fst; snd := snd |})
+  (p : prod A B) =>
+match p as p0 return (P p0) with
+| {| fst := x; snd := x0 |} => f x x0
+end
+     : forall (A B : Type) (P : prod A B -> Type),
+       (forall (fst : A) (snd : B), P {| fst := fst; snd := snd |}) ->
+       forall p : prod A B, P p
+
+Arguments A, B are implicit
+Argument scopes are [type_scope type_scope _ _ _]
+ *)
+
+(* What I really want: *)
+Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B), P (pair fst snd))
+           (p : prod A B) : P p
+  := u (fst p) (snd p).
+
+Notation typeof x := ($(let T := type of x in exact T)$) (only parsing).
+
+(* Check for eta *)
+Check eq_refl : typeof (@prod_rect) = typeof (@prod_rect').
+
+(* Check for the recursion principle I want *)
+Fail Check eq_refl : @prod_rect = @prod_rect'.
diff --git a/test-suite/bugs/opened/HoTT_coq_093.v b/test-suite/bugs/opened/HoTT_coq_093.v
new file mode 100644
index 000000000..029a0caf7
--- /dev/null
+++ b/test-suite/bugs/opened/HoTT_coq_093.v
@@ -0,0 +1,37 @@
+(** It would be nice if we had more lax constraint checking of inductive types, and had variance annotations on their universes *)
+Set Printing All.
+Set Printing Implicit.
+Set Printing Universes.
+Set Universe Polymorphism.
+
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+
+Notation "x = y" := (@paths _ x y) : type_scope.
+
+Section lift.
+  Let lift_type : Type.
+  Proof.
+    let U0 := constr:(Type) in
+    let U1 := constr:(Type) in
+    let unif := constr:(U0 : U1) in
+    exact (U0 -> U1).
+  Defined.
+
+  Definition Lift : lift_type := fun A => A.
+End lift.
+
+Goal forall (A : Type) (x y : A), @paths A x y -> @paths (Lift A) x y.
+intros A x y p.
+compute in *.
+Fail exact p. (* Toplevel input, characters 21-22:
+Error:
+In environment
+A : Type (* Top.15 *)
+x : A
+y : A
+p : @paths (* Top.15 *) A x y
+The term "p" has type "@paths (* Top.15 *) A x y"
+while it is expected to have type "@paths (* Top.18 *) A x y"
+(Universe inconsistency: Cannot enforce Top.18 = Top.15 because Top.15
+< Top.18)). *)
diff --git a/test-suite/bugs/opened/HoTT_coq_114.v b/test-suite/bugs/opened/HoTT_coq_114.v
new file mode 100644
index 000000000..e293e6dbb
--- /dev/null
+++ b/test-suite/bugs/opened/HoTT_coq_114.v
@@ -0,0 +1,2 @@
+Fail Inductive test : $(let U := type of Type in exact U)$ := t.
+(* Anomaly: Unable to handle arbitrary u+k <= v constraints. Please report. *)