8 files changed, 53 insertions, 1 deletions
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index ca8da3948..ee540d710 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -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 29350d620..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
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 5b13f35d5..253b48e4d 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -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/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/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.