Merge branch 'v8.6'

4 files changed, 36 insertions, 1 deletions

diff --git a/test-suite/bugs/closed/4970.v b/test-suite/bugs/closed/4970.v
new file mode 100644
index 0000000000..7a896582f5
--- /dev/null
+++ b/test-suite/bugs/closed/4970.v
@@ -0,0 +1,3 @@
+(* Check "{{" is not confused with "{" in notations *)
+Reserved Notation "x {{ y }}" (at level 40).
+Notation "x {{ y }}" := (x y) (only parsing).
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 8745cf2fbd..da2183841d 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -135,6 +135,21 @@ intros * [= H].
 exact H.
 Abort.
 
+(* Test the Keep Proof Equalities option. *)
+Set Keep Proof Equalities.
+Unset Structural Injection.
+
+Inductive pbool : Prop := Pbool1 | Pbool2.
+
+Inductive pbool_shell : Set := Pbsc : pbool -> pbool_shell.
+
+Goal Pbsc Pbool1 = Pbsc Pbool2 -> True.
+injection 1.
+match goal with
+ |- Pbool1 = Pbool2 -> True => idtac | |- True => fail
+end.
+Abort.
+
 (* Injection does not project at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index c9c7c611cc..4db547f4e4 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -117,7 +117,7 @@ Lemma simpl_plus_l_rr1 :
   Undo.
   Set Typeclasses Debug.
   Set Typeclasses Iterative Deepening.
-  Time typeclasses eauto 2 with nocore. Show Proof.
+  Time typeclasses eauto 6 with nocore. Show Proof.
   Undo.
   Time eauto. (* does EApply H *)
 Qed.
diff --git a/test-suite/success/subst.v b/test-suite/success/subst.v
index 8336f6a806..25ee81b587 100644
--- a/test-suite/success/subst.v
+++ b/test-suite/success/subst.v
@@ -23,3 +23,20 @@ subst.
 change (y = S (S y)) in H0.
 change (S y = y).
 Abort.
+
+(* A bug revealed by OCaml 4.03 warnings *)
+(* fixes in 4e3d464 and 89ec88f for v8.5, 4e3d4646 and 89ec88f1e for v8.6 *)
+Goal forall y, let x:=0 in y=x -> y=y.
+intros * H;
+(* This worked as expected *)
+subst.
+Fail clear H.
+Abort.
+
+Goal forall y, let x:=0 in x=y -> y=y.
+intros * H;
+(* Before the fix, this unfolded x instead of 
+   substituting y and erasing H *)
+subst.
+Fail clear H.
+Abort.