From fd47b2d2638518fe62ce9c63557d2dab219d9558 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin <cyprien.mangin@m4x.org>
Date: Thu, 30 Jun 2016 19:41:53 +0200
Subject: Goal selectors now use the keyword [only].

This fixes some parsing problems when doing things like
[let n := 2 in idtac n]. See bug #4877.
---
 test-suite/success/goal_selector.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'test-suite/success')

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


From 8e0f29cb69f06b64d74b18b09fb6a717034f1140 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Mon, 22 Aug 2016 08:32:59 +0200
Subject: Typeclass backtracking example by J. Leivant

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

(limited to 'test-suite/success')

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


From a6832ccfacd9c105b23a9a77dadc3202f7af26fc Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Thu, 29 Sep 2016 10:46:53 +0200
Subject: Argument : assert does fail if no arg is given (fix #4864)

---
 test-suite/output/Arguments.v     | 2 +-
 test-suite/success/simpl_tuning.v | 2 +-
 toplevel/vernacentries.ml         | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'test-suite/success')

diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 05eeaac63..bd9240476 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -17,7 +17,7 @@ Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
 Arguments fcomp {_ _ _}%type_scope f g x /.
 About fcomp.
 Definition volatile := fun x : nat => x.
-Arguments volatile /.
+Arguments volatile / _.
 About volatile.
 Set Implicit Arguments.
 Section S1.
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.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 48a85b709..382a71629 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -986,9 +986,9 @@ let vernac_declare_arguments locality r l nargs flags =
     | _::li, _::ld, _::ls -> check li ld ls 
     | _ -> assert false in
   let () = match l with
-  | [[]] -> ()
+  | [[]] when List.exists ((<>) `Assert) flags -> ()
   | _ ->
-    List.iter2 (fun l -> check inf_names l) (names :: rest) scopes
+    List.iter2 (check inf_names) (names :: rest) scopes
   in
   (* we take extra scopes apart, and we check they are consistent *)
   let l, scopes = 
-- 
cgit v1.2.3