Merge branch 'v8.5'

4 files changed, 96 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4498.v b/test-suite/bugs/closed/4498.v
new file mode 100644
index 000000000..ccdb2dddd
--- /dev/null
+++ b/test-suite/bugs/closed/4498.v
@@ -0,0 +1,24 @@
+Require Export Coq.Unicode.Utf8.
+Require Export Coq.Classes.Morphisms.
+Require Export Coq.Relations.Relation_Definitions.
+
+Set Universe Polymorphism.
+
+Reserved Notation "a ~> b" (at level 90, right associativity).
+
+Class Category := {
+  ob            : Type;
+  uhom          := Type : Type;
+  hom           : ob → ob → uhom where "a ~> b" := (hom a b);
+  compose       : ∀ {A B C}, (B ~> C) → (A ~> B) → (A ~> C);
+  equiv         : ∀ {A B}, relation (A ~> B);
+  is_equiv      : ∀ {A B}, @Equivalence (A ~> B) equiv;
+  comp_respects : ∀ {A B C},
+      Proper (@equiv B C ==> @equiv A B ==> @equiv A C) (@compose A B C);
+}.
+
+Require Export Coq.Setoids.Setoid.
+
+Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with
+  signature equiv ==> equiv ==> equiv as compose_mor.
+Proof. apply comp_respects. Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4628.v b/test-suite/bugs/closed/4628.v
new file mode 100644
index 000000000..7d4a15d68
--- /dev/null
+++ b/test-suite/bugs/closed/4628.v
@@ -0,0 +1,46 @@
+Module first.
+  Polymorphic Record BAR (A:Type) :=
+  { foo: A->Prop; bar: forall (x y: A), foo x -> foo y}.
+
+Section A.
+Context {A:Type}.
+
+Set Printing Universes.
+
+Hint Resolve bar.
+Goal forall (P:BAR A) x y, foo _ P x -> foo _ P y.
+intros.
+eauto.
+Qed.
+End A.
+End first.
+
+Module firstbest.
+  Polymorphic Record BAR (A:Type) :=
+  { foo: A->Prop; bar: forall (x y: A), foo x -> foo y}.
+
+Section A.
+Context {A:Type}.
+
+Set Printing Universes.
+
+Polymorphic Hint Resolve bar.
+Goal forall (P:BAR A) x y, foo _ P x -> foo _ P y.
+intros.
+eauto.
+Qed.
+End A.
+End firstbest.
+
+Module second.
+Axiom foo: Set.
+Axiom foo': Set.
+
+Polymorphic Record BAR (A:Type) :=
+  { bar: foo' -> foo}.
+Set Printing Universes.
+
+Lemma baz@{i}: forall (P:BAR@{Set} nat), foo' -> foo.
+  eauto using bar.
+Qed.
+End second.
diff --git a/test-suite/bugs/closed/4710.v b/test-suite/bugs/closed/4710.v
new file mode 100644
index 000000000..fdc850109
--- /dev/null
+++ b/test-suite/bugs/closed/4710.v
@@ -0,0 +1,12 @@
+Set Primitive Projections.
+Record Foo' := Foo { foo : nat }.
+Extraction foo.
+Record Foo2 (a : nat) := Foo2c { foo2p : nat; foo2b : bool }.
+Extraction Language Ocaml.
+Extraction foo2p.
+
+Definition bla (x : Foo2 0) := foo2p _ x.
+Extraction bla.
+
+Definition bla' (a : nat) (x : Foo2 a) := foo2b _ x.
+Extraction bla'.
diff --git a/test-suite/bugs/closed/4746.v b/test-suite/bugs/closed/4746.v
new file mode 100644
index 000000000..d64cc6fe6
--- /dev/null
+++ b/test-suite/bugs/closed/4746.v
@@ -0,0 +1,14 @@
+Variables P Q : nat -> Prop.
+Variable f : nat -> nat.
+
+Goal forall (x:nat), (forall y, P y -> forall z, Q z -> y=f z -> False) -> False.
+Proof.
+intros.
+ecase H with (3:=eq_refl).
+Abort.
+
+Goal forall (x:nat), (forall y, y=x -> False) -> False.
+Proof.
+intros.
+unshelve ecase H with (1:=eq_refl).
+Qed.