Merge branch 'v8.5'

5 files changed, 60 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3900.v b/test-suite/bugs/closed/3900.v
new file mode 100644
index 0000000000..6be2161c2f
--- /dev/null
+++ b/test-suite/bugs/closed/3900.v
@@ -0,0 +1,13 @@
+Global Set Primitive Projections.
+Set Implicit Arguments.
+Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Variable A : PreCategory.
+Variable Pobj : A -> Type.
+Local Notation obj := (sigT Pobj).
+Variable Pmor : forall s d : obj, morphism A (projT1 s) (projT1 d) -> Type.
+Class Foo (x : Type) := { _ : forall y, y }.
+Local Instance ishset_pmor {s d m} : Foo (Pmor s d m).
+Proof.
+SearchAbout ((forall _ _, _) -> Foo _).
+Abort.
diff --git a/test-suite/bugs/closed/4001.v b/test-suite/bugs/closed/4001.v
new file mode 100644
index 0000000000..25d78f4b0e
--- /dev/null
+++ b/test-suite/bugs/closed/4001.v
@@ -0,0 +1,18 @@
+(* Computing the type constraints to be satisfied when building the
+   return clause of a match with a match *)
+
+Set Implicit Arguments.
+Set Asymmetric Patterns.
+  
+Variable A : Type.
+Variable typ : A -> Type.
+
+Inductive t : list A -> Type :=
+| snil  : t nil
+| scons : forall (x : A) (e : typ x) (lx : list A) (le : t  lx), t (x::lx).
+
+Definition car (x:A) (lx : list A) (s: t (x::lx)) : typ x :=
+  match s in t l'  with
+  | snil => False
+  | scons _ e _ _ => e
+  end.
diff --git a/test-suite/bugs/closed/4017.v b/test-suite/bugs/closed/4017.v
new file mode 100644
index 0000000000..a6f177b496
--- /dev/null
+++ b/test-suite/bugs/closed/4017.v
@@ -0,0 +1,6 @@
+(* Use of implicit arguments was lost in multiple variable declarations *)
+Variables 
+  (A1 : Type)
+  (A2 : forall (x1 : A1), Type) 
+  (A3 : forall (x1 : A1) (x2 : A2 x1), Type)
+  (A4 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2), Type).
diff --git a/test-suite/bugs/closed/4018.v b/test-suite/bugs/closed/4018.v
new file mode 100644
index 0000000000..c3a045943c
--- /dev/null
+++ b/test-suite/bugs/closed/4018.v
@@ -0,0 +1,3 @@
+(* Catching PatternMatchingFailure was lost at some point *)
+Goal nat -> True.
+intros [=].
diff --git a/test-suite/success/TacticNotation1.v b/test-suite/success/TacticNotation1.v
new file mode 100644
index 0000000000..289f2816e5
--- /dev/null
+++ b/test-suite/success/TacticNotation1.v
@@ -0,0 +1,20 @@
+Module Type S.
+End S.
+
+Module F (E : S).
+
+  Tactic Notation "foo" := idtac.
+
+  Ltac bar := foo.
+
+End F.
+
+Module G (E : S).
+  Module M := F E.
+
+  Lemma Foo : True.
+  Proof.
+  M.bar.
+  Abort.
+
+End G.