From 24d5448c65ba05072a5ab4180c9be95670ce126d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 30 Sep 2016 18:59:11 +0200
Subject: More tests for tactic "subst".

---
 test-suite/success/subst.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From 0746578040e738d079bcc3289857bb99983a7a22 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 30 Sep 2016 11:52:21 +0200
Subject: fixing bug 4609: document an option governing the generation of
 equalities between proofs in tactic injection, with a side-effect on
 inversion.

---
 test-suite/success/Injection.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From 14f8db195021e709734ed89d9cb513d1c0db6a93 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 3 Oct 2016 22:12:56 +0200
Subject: Fixing #4970 (confusion between special "{" and non special "{{" in
 notations).

---
 test-suite/bugs/closed/4970.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/4970.v

(limited to 'test-suite')

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).
-- 
cgit v1.2.3


From e2c0b6711ab100c1dc4d103601a951688b115c7c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 5 Oct 2016 12:05:39 +0200
Subject: Clean up type classes flags and update compat file.

---
 test-suite/success/eauto.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3