21 files changed, 98 insertions, 28 deletions

diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v
index b4efa7edc..d0aa5c857 100644
--- a/test-suite/success/AdvancedTypeClasses.v
+++ b/test-suite/success/AdvancedTypeClasses.v
@@ -28,8 +28,8 @@ Class interp_pair (abs : Type) :=
  { repr : term;
   link: abs = interp repr }.
 
-Implicit Arguments repr [[interp_pair]].
-Implicit Arguments link [[interp_pair]].
+Arguments repr _ {interp_pair}.
+Arguments link _ {interp_pair}.
 
 Lemma prod_interp `{interp_pair a, interp_pair b} : a * b = interp (Prod (repr a) (repr b)).
   simpl. intros. rewrite <- link. rewrite <- (link b). reflexivity.
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index 921433cad..9a19b595e 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -2,7 +2,7 @@ Inductive vector {A : Type} : nat -> Type :=
 | vnil : vector 0
 | vcons : A -> forall {n'}, vector n' -> vector (S n').
 
-Implicit Arguments vector [].
+Arguments vector A : clear implicits.
 
 Require Import Coq.Program.Program.
 
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 5b1482fd5..f07c0191f 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -73,7 +73,7 @@ CoInductive LList (A : Set) : Set :=
   | LNil : LList A
   | LCons : A -> LList A -> LList A.
 
-Implicit Arguments LNil [A].
+Arguments LNil [A].
 
 Inductive Finite (A : Set) : LList A -> Prop :=
   | Finite_LNil : Finite LNil
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 45c71615f..ee540d710 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type :=
   | in_first : forall e, in_extension r (add_rule r e)
   | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e).
 
-Implicit Arguments NL [I].
+Arguments NL [I].
 
 Inductive super_extension (I : Set) (e : extension I) :
 extension I -> Type :=
@@ -107,6 +107,7 @@ Goal forall o, foo2 o -> 0 = 1.
 intros.
 eapply trans_eq.
 inversion H.
+Abort.
 
 (* Check that the part of "injection" that is called by "inversion"
    does the same number of intros as the number of equations
@@ -136,6 +137,7 @@ Goal True -> True.
 intro.
 Fail inversion H using False.
 Fail inversion foo using True_ind.
+Abort.
 
 (* Was failing at some time between 7 and 10 September 2014 *)
 (* even though, it is not clear that the resulting context is interesting *)
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 841940492..6370cab6b 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -589,6 +589,8 @@ Close Scope Z_scope.
 
 Theorem S_is_not_O : forall n, S n <> 0.
 
+Set Nested Proofs Allowed.
+
 Definition Is_zero (x:nat):= match x with
                                      | 0 => True
                                      | _ => False
@@ -991,10 +993,10 @@ Proof.
 Qed.
 
 
-Implicit Arguments Vector.cons [A n].
-Implicit Arguments Vector.nil [A].
-Implicit Arguments Vector.hd [A n].
-Implicit Arguments Vector.tl [A n].
+Arguments Vector.cons [A] _ [n].
+Arguments Vector.nil [A].
+Arguments Vector.hd [A n].
+Arguments Vector.tl [A n].
 
 Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n.
 Proof.
@@ -1064,7 +1066,7 @@ Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v}
   | S n', Vector.cons _ v' => vector_nth A n' _ v'
   end.
 
-Implicit Arguments vector_nth [A p].
+Arguments vector_nth [A] _ [p].
 
 
 Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i  a b,
@@ -1159,7 +1161,7 @@ infiniteproof map_iterate'.
 Qed.
 
 
-Implicit Arguments LNil [A].
+Arguments LNil [A].
 
 Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A),
                                LNil <> (LCons a l).
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 6f27c1d36..18ebcd638 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -5,7 +5,7 @@ Require Import Program.
 Require Import List.
 
 Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }.
-Implicit Arguments vector [].
+Arguments vector : clear implicits.
 
 Coercion vec_list : vector >-> list.
 
diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v
index ca3746716..2da630633 100644
--- a/test-suite/success/Scopes.v
+++ b/test-suite/success/Scopes.v
@@ -11,7 +11,7 @@ Check (A.opp 3).
 
 Record B := { f :> Z -> Z }.
 Variable a:B.
-Arguments Scope a [Z_scope].
+Arguments a _%Z_scope : extra scopes.
 Check a 0.
 
 (* Check that casts activate scopes if ever possible *)
diff --git a/test-suite/success/ShowExtraction.v b/test-suite/success/ShowExtraction.v
index e34c240c5..a4a35003d 100644
--- a/test-suite/success/ShowExtraction.v
+++ b/test-suite/success/ShowExtraction.v
@@ -12,7 +12,7 @@ Fail Show Extraction.
 Lemma decListA : forall (xs ys : list A), {xs=ys}+{xs<>ys}.
 Proof.
 Show Extraction.
-fix 1.
+fix decListA 1.
 destruct xs as [|x xs], ys as [|y ys].
 Show Extraction.
 - now left.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index cd6eac35c..400479ae8 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -128,8 +128,8 @@ Record Monad {m : Type -> Type} := {
 
 Print Visibility.
 Print unit.
-Implicit Arguments unit [[m] [m0] [α]].
-Implicit Arguments Monad [].
+Arguments unit {m m0 α}.
+Arguments Monad : clear implicits.
 Notation "'return' t" := (unit t).
 
 (* Test correct handling of existentials and defined fields. *)
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 02e043bc3..b287b5fac 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -39,7 +39,7 @@ Qed.
 (* Check apply/eapply distinction in presence of open terms *)
 
 Parameter h : forall x y z : nat, x = z -> x = y.
-Implicit Arguments h [[x] [y]].
+Arguments h {x y}.
 Goal 1 = 0 -> True.
 intro H.
 apply h in H || exact I.
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index bbfe5ec42..49a8b9cf4 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -151,3 +151,17 @@ Section JLeivant.
     congruence.
   Qed.
 End JLeivant.
+
+(* An example with primitive projections *)
+
+Module PrimitiveProjections.
+Set Primitive Projections.
+Record t (A:Type) := { f : A }.
+Goal forall g (a:t nat), @f nat = g -> f a = 0 -> g a = 0.
+congruence.
+Undo.
+intros.
+unfold f in H0. (* internally turn the projection to unfolded form *)
+congruence.
+Qed.
+End PrimitiveProjections.
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index f5bb884d2..55ae54ca0 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -42,7 +42,7 @@ Inductive ctx : Type :=
 Bind Scope context_scope with ctx.
 Delimit Scope context_scope with ctx.
 
-Arguments Scope snoc [context_scope].
+Arguments snoc _%context_scope.
 
 Notation " Γ , τ " := (snoc Γ τ) (at level 25, τ at next level, left associativity) : context_scope.
 
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 6fbe61a9b..d1d384659 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -422,6 +422,7 @@ Abort.
 Goal forall b:bool, b = b.
 intros.
 destruct b eqn:H.
+Abort.
 
 (* Check natural instantiation behavior when the goal has already an evar *)
 
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 627794832..253b48e4d 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -386,7 +386,7 @@ Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }.
 Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri {
   tri0 : forall a b c, R a b -> S a c -> T b c
 }.
-Implicit Arguments mkTri [R S T].
+Arguments mkTri [R S T].
 Definition tri_iffT : tri iffT iffT iffT :=
   (mkTri
     (fun X0 X1 X2 E01 E02 =>
@@ -421,3 +421,8 @@ Goal exists n : nat, n = n -> True.
 eexists.
 set (H := _ = _).
 Abort.
+
+(* Check interpretation of default evar instance in pretyping *)
+(* (reported as bug #7356) *)
+
+Check fun (P : nat -> Prop) (x:nat) (h:P x) => exist _ ?[z] (h : P ?z).
diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v
index 868140517..0951c5c8d 100644
--- a/test-suite/success/goal_selector.v
+++ b/test-suite/success/goal_selector.v
@@ -53,3 +53,17 @@ Goal True -> exists (x : Prop), x.
 Proof.
   intro H; eexists ?[x]; only [x]: exact True. 1: assumption.
 Qed.
+
+(* Strict focusing! *)
+Set Default Goal Selector "!".
+
+Goal True -> True /\ True /\ True.
+Proof.
+  intro.
+  split;only 2:split.
+  Fail exact I.
+  Fail !:exact I.
+  1:exact I.
+  - !:exact H.
+  - exact I.
+Qed.
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index a0981311b..23853890d 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -33,11 +33,11 @@ Definition eq1 := fun (A:Type) (x y:A) => x=y.
 Definition eq2 := fun (A:Type) (x y:A) => x=y.
 Definition eq3 := fun (A:Type) (x y:A) => x=y.
 
-Implicit Arguments op' [].
-Global Implicit Arguments op'' [].
+Arguments op' : clear implicits.
+Global Arguments op'' : clear implicits.
 
-Implicit Arguments eq2 [].
-Global Implicit Arguments eq3 [].
+Arguments eq2 : clear implicits.
+Global Arguments eq3 : clear implicits.
 
 Check (op 0 0).
 Check (op' nat 0 0).
@@ -89,14 +89,14 @@ Fixpoint plus n m {struct n} :=
 
 (* Check multiple implicit arguments signatures *)
 
-Implicit Arguments eq_refl [[A] [x]] [[A]].
+Arguments eq_refl {A x}, {A}.
 
 Check eq_refl : 0 = 0.
 
 (* Check that notations preserve implicit (since 8.3) *)
 
 Parameter p : forall A, A -> forall n, n = 0 -> True.
-Implicit Arguments p [A n].
+Arguments p [A] _ [n].
 Notation Q := (p 0).
 Check Q eq_refl.
 
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index a329894aa..d37ad9f52 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -127,4 +127,28 @@ induction 1 as (n,H,IH).
 exact Logic.I.
 Qed.
 
+(* Make "intro"/"intros" progress on existential variables *)
 
+Module Evar.
+
+Goal exists (A:Prop), A.
+eexists.
+unshelve (intro x).
+- exact nat.
+- exact (x=x).
+- auto.
+Qed.
+
+Goal exists (A:Prop), A.
+eexists.
+unshelve (intros x).
+- exact nat.
+- exact (x=x).
+- auto.
+Qed.
+
+Definition d := ltac:(intro x; exact (x*x)).
+
+Definition d' : nat -> _ := ltac:(intros;exact 0).
+
+End Evar.
diff --git a/test-suite/success/name_mangling.v b/test-suite/success/name_mangling.v
index 571dde880..e98241420 100644
--- a/test-suite/success/name_mangling.v
+++ b/test-suite/success/name_mangling.v
@@ -122,8 +122,7 @@ Lemma a : forall n, n = 0.
 Proof.
 fix a 1.
 Check a.
-fix 1.
-Fail Check a0.
+Fail fix a 1.
 Abort.
 
 (* Test stability of "induction" *)
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index 22fb4d757..40986e57c 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -121,14 +121,16 @@ Abort.
 (* Wish 1988: that fun forces unfold in refine *)
 
 Goal (forall A : Prop, A -> ~~A).
-Proof. refine(fun A a f => _).
+Proof. refine(fun A a f => _). Abort.
 
 (* Checking beta-iota normalization of hypotheses in created evars *)
 
 Goal {x|x=0} -> True.
 refine (fun y => let (x,a) := y in _).
 match goal with a:_=0 |- _ => idtac end.
+Abort.
 
 Goal (forall P, {P 0}+{P 1}) -> True.
 refine (fun H => if H (fun x => x=x) then _ else _).
 match goal with _:0=0 |- _ => idtac end.
+Abort.
diff --git a/test-suite/success/sideff.v b/test-suite/success/sideff.v
index 3c0b81568..b9a1273b1 100644
--- a/test-suite/success/sideff.v
+++ b/test-suite/success/sideff.v
@@ -5,6 +5,8 @@ Proof.
   apply (const tt tt).
 Qed.
 
+Set Nested Proofs Allowed.
+
 Lemma foobar' : unit.
   Lemma aux : forall A : Type, A -> unit.
   Proof. intros. pose (foo := idw A). exact tt. Show Universes. Qed.
diff --git a/test-suite/success/ssr_delayed_clear_rename.v b/test-suite/success/ssr_delayed_clear_rename.v
new file mode 100644
index 000000000..951e5aff7
--- /dev/null
+++ b/test-suite/success/ssr_delayed_clear_rename.v
@@ -0,0 +1,5 @@
+Require Import ssreflect.
+Example foo (t t1 t2 : True) : True /\ True -> True -> True.
+Proof.
+move=>[{t1 t2 t} t1 t2] t.
+Abort.