Merge branch 'v8.5'

7 files changed, 52 insertions, 1 deletions

diff --git a/test-suite/bugs/opened/3593.v b/test-suite/bugs/closed/3593.v
index d83b90060..378db6857 100644
--- a/test-suite/bugs/opened/3593.v
+++ b/test-suite/bugs/closed/3593.v
@@ -5,6 +5,6 @@ Record prod A B := pair { fst : A ; snd : B }.
 Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x.
 simpl; intros.
   constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x).   
-  Fail Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x).
+  Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x).
   reflexivity.
 Qed.
diff --git a/test-suite/bugs/closed/4190.v b/test-suite/bugs/closed/4190.v
new file mode 100644
index 000000000..2843488ba
--- /dev/null
+++ b/test-suite/bugs/closed/4190.v
@@ -0,0 +1,15 @@
+Module Type A .
+ Tactic Notation "bar" := idtac "ITSME".
+End A.
+
+Module Type B.
+ Tactic Notation "foo" := fail "NOTME".
+End B.
+
+Module Type C := A <+ B.
+
+Module Type F (Import M : C).
+
+Lemma foo : True.
+Proof.
+bar.
diff --git a/test-suite/bugs/closed/4191.v b/test-suite/bugs/closed/4191.v
new file mode 100644
index 000000000..290bb384d
--- /dev/null
+++ b/test-suite/bugs/closed/4191.v
@@ -0,0 +1,5 @@
+(* Test maximal implicit arguments in the presence of let-ins *)
+Definition foo (x := 1) {y : nat} (H : y = y) : True := I.
+Definition bar {y : nat} (x := 1) (H : y = y) : True := I.
+Check bar (eq_refl 1).
+Check foo (eq_refl 1). 
diff --git a/test-suite/bugs/closed/4193.v b/test-suite/bugs/closed/4193.v
new file mode 100644
index 000000000..885d04a92
--- /dev/null
+++ b/test-suite/bugs/closed/4193.v
@@ -0,0 +1,7 @@
+Module Type E.
+End E.
+
+Module Type A (M : E).
+End A.
+
+Fail Module Type F (Import X : A).
diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
new file mode 100644
index 000000000..ef991365d
--- /dev/null
+++ b/test-suite/bugs/closed/4198.v
@@ -0,0 +1,13 @@
+Require Import List.
+Open Scope list_scope.
+Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
+       let k :=
+           (match H in (_ = y) return x = hd x y with
+              | eq_refl => eq_refl
+            end : x = x')
+       in k = k.
+  simpl.
+  intros.
+  match goal with
+    | [ |- appcontext G[@hd] ] => idtac
+  end.
diff --git a/test-suite/bugs/closed/4214.v b/test-suite/bugs/closed/4214.v
new file mode 100644
index 000000000..cd53c898e
--- /dev/null
+++ b/test-suite/bugs/closed/4214.v
@@ -0,0 +1,5 @@
+(* Check that subst uses all equations around *)
+Goal forall A (a b c : A), b = a -> b = c -> a = c.
+intros.
+subst.
+reflexivity.
diff --git a/test-suite/bugs/closed/4217.v b/test-suite/bugs/closed/4217.v
new file mode 100644
index 000000000..19973f30a
--- /dev/null
+++ b/test-suite/bugs/closed/4217.v
@@ -0,0 +1,6 @@
+(* Checking correct index of implicit by pos in fixpoints *)
+
+Fixpoint ith_default
+         {default_A : nat}
+         {As : list nat}
+         {struct As} : Set.