Merge branch 'v8.6'

3 files changed, 24 insertions, 5 deletions

diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 590f6e191..bb1cf0654 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -46,6 +46,25 @@ Module Backtracking.
   Qed.
   
   Unset Typeclasses Debug.
+
+  Module Leivant.
+    Axiom A : Type.
+    Existing Class A.
+    Axioms a b c d e: A.
+    
+    Ltac get_value H := eval cbv delta [H] in H.
+    
+    Goal True.
+      Fail refine (let H := _ : A in _); let v := get_value H in idtac v; fail.
+    Admitted.
+
+    Goal exists x:A, x=a.
+      unshelve evar (t : A). all:cycle 1.
+      refine (@ex_intro _ _ t _).
+      all:cycle 1.
+      all:(typeclasses eauto + reflexivity).
+    Qed.      
+  End Leivant.
 End Backtracking.
 
 
diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v
index 91fb54d9a..868140517 100644
--- a/test-suite/success/goal_selector.v
+++ b/test-suite/success/goal_selector.v
@@ -34,7 +34,7 @@ Qed.
 
 Goal True -> True.
 Proof.
-  intros y; 1-2 : repeat idtac.
+  intros y; only 1-2 : repeat idtac.
   1-1:match goal with y : _ |- _ => let x := y in idtac x end.
   Fail 1-1:let x := y in idtac x.
   1:let x := y in idtac x.
@@ -44,12 +44,12 @@ Qed.
 Goal True /\ (True /\ True).
 Proof.
   dup.
-  - split; 2: (split; exact I).
+  - split; only 2: (split; exact I).
     exact I.
-  - split; 2: split; exact I.
+  - split; only 2: split; exact I.
 Qed.
 
 Goal True -> exists (x : Prop), x.
 Proof.
-  intro H; eexists ?[x]. [x]: exact True. 1: assumption.
+  intro H; eexists ?[x]; only [x]: exact True. 1: assumption.
 Qed.
diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v
index d4191b939..2728672f3 100644
--- a/test-suite/success/simpl_tuning.v
+++ b/test-suite/success/simpl_tuning.v
@@ -106,7 +106,7 @@ match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end.
 Abort. 
 
 Definition volatile := fun x : nat => x.
-Arguments volatile /.
+Arguments volatile / _.
 
 Lemma foo : volatile = volatile.
 simpl.