Merge branch 'v8.5'

3 files changed, 33 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3779.v b/test-suite/bugs/closed/3779.v
new file mode 100644
index 0000000000..eb0d206c5c
--- /dev/null
+++ b/test-suite/bugs/closed/3779.v
@@ -0,0 +1,11 @@
+Set Universe Polymorphism.
+Record UnitSubuniverse := { a : Type@{sm} ; x : (Type@{sm} : Type@{lg}) ; inO_internal : Type@{lg} -> Type@{lg} }.
+Class In (O : UnitSubuniverse@{sm lg}) (T : Type@{lg}) := in_inO_internal : inO_internal O T.
+Section foo.
+  Universes sm lg.
+  Context (O : UnitSubuniverse@{sm lg}).
+  Context {A : Type@{sm}}.
+  Context (H' : forall (C : Type@{lg}) `{In@{sm lg} O C} (f : A -> C), In@{sm lg} O C).
+  Fail Check (H' : forall (C : Type@{lg}) `{In@{i j} O C} (f : A -> C), In@{j i} O C).
+  Fail Context (H'' : forall (C : Type@{lg}) `{In@{i j} O C} (f : A -> C), In@{j i} O C).
+End foo.
diff --git a/test-suite/bugs/closed/4221.v b/test-suite/bugs/closed/4221.v
new file mode 100644
index 0000000000..bc120fb1ff
--- /dev/null
+++ b/test-suite/bugs/closed/4221.v
@@ -0,0 +1,9 @@
+(* Some test checking that interpreting binder names using ltac
+   context does not accidentally break the bindings *)
+
+Goal (forall x : nat, x = 1 -> False) -> 1 = 1 -> False.
+  intros H0 x.
+  lazymatch goal with
+    | [ x : forall k : nat, _ |- _ ]
+      => specialize (fun H0 => x 1 H0)
+  end.
diff --git a/test-suite/bugs/closed/4254.v b/test-suite/bugs/closed/4254.v
new file mode 100644
index 0000000000..ef219973df
--- /dev/null
+++ b/test-suite/bugs/closed/4254.v
@@ -0,0 +1,13 @@
+Inductive foo (V:Type):Type :=
+  | Foo : list (bar V) -> foo V
+with bar (V:Type): Type :=
+  | bar1: bar V
+  | bar2 : V -> bar V.
+
+Module WithPoly.
+Polymorphic Inductive foo (V:Type):Type :=
+  | Foo : list (bar V) -> foo V
+with bar (V:Type): Type :=
+  | bar1: bar V
+  | bar2 : V -> bar V.
+End WithPoly.