Updating test-suite after Bracketing Last Introduction Pattern set by

default. Interestingly, there is an example where it makes the rest of
the proof less natural.

Goal forall x y:Z, ...
intros [y|p1[|p2|p2]|p1[|p2|p2]].

where case analysis on y is not only in the 2nd and 3rd case, is not
anymore easy to do.

Still, I find the bracketing of intro-patterns a natural property, and
its generalization in all situations a natural expectation for
uniformity. So, what to do? The following is e.g. not as compact and
"one-shot":

intros [|p1|p1]; [intros y|intros [|p2|p2] ..].

3 files changed, 12 insertions, 13 deletions

diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index 8767f6874..abf8be72e 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -53,8 +53,7 @@ Qed.
 
 Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1.
 Proof.
- unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Z.mul_1_r.
- intros HQeq.
+ unfold Qeq; intros (x,HQeq); simpl (Qden (2#1)) in HQeq; rewrite Z.mul_1_r in HQeq.
  assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by
    (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto).
  assert (Hnx : (Qnum x <> 0)%Z)
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4116a5ebc..a95b085ac 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -73,7 +73,7 @@ Definition f : B -> True.
 
 Proof.
 intros [].
-destruct b as [|] ; intros _ ; exact Logic.I.
+destruct b as [|] ; exact Logic.I.
 Defined.
 
 Print f.
diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
index 0d75d52a3..06357cfc2 100644
--- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
+++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
@@ -1902,14 +1902,14 @@ Qed.
 
 Lemma Zsgn_15 : forall x y : Z, Zsgn (x * y) = (Zsgn x * Zsgn y)%Z.
 Proof.
- intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; constructor.
+ intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; constructor.
 Qed.
 
 Lemma Zsgn_16 :
  forall x y : Z,
  Zsgn (x * y) = 1%Z -> {(0 < x)%Z /\ (0 < y)%Z} + {(x < 0)%Z /\ (y < 0)%Z}.
 Proof.
- intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H;
+ intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   try discriminate H; [ left | right ]; repeat split.
 Qed. 
 
@@ -1917,13 +1917,13 @@ Lemma Zsgn_17 :
  forall x y : Z,
  Zsgn (x * y) = (-1)%Z -> {(0 < x)%Z /\ (y < 0)%Z} + {(x < 0)%Z /\ (0 < y)%Z}.
 Proof.
- intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H;
+ intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   try discriminate H; [ left | right ]; repeat split.
 Qed. 
 
 Lemma Zsgn_18 : forall x y : Z, Zsgn (x * y) = 0%Z -> {x = 0%Z} + {y = 0%Z}.
 Proof.
- intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H;
+ intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   try discriminate H; [ left | right | right ]; constructor.
 Qed. 
 
@@ -1932,40 +1932,40 @@ Qed.
 Lemma Zsgn_19 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 < x + y)%Z.
 Proof.
  Proof.
- intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H;
+ intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   discriminate H || (constructor || apply Zsgn_12; assumption).
 Qed.
 
 Lemma Zsgn_20 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (x + y < 0)%Z.
 Proof.
  Proof.
- intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H;
+ intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   discriminate H || (constructor || apply Zsgn_11; assumption).
 Qed.
 
 
 Lemma Zsgn_21 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 <= x)%Z.
 Proof.
- intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intros H H0;
+ intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intros H H0;
   discriminate H || discriminate H0.
 Qed.
 
 Lemma Zsgn_22 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (x <= 0)%Z.
 Proof.
  Proof.
- intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intros H H0;
+ intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intros H H0;
   discriminate H || discriminate H0.
 Qed.
 
 Lemma Zsgn_23 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 <= y)%Z.
 Proof.
- intros [[| p2| p2]| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *;
+ intros [|p1|p1] [|p2|p2]; simpl in |- *;
   intros H H0; discriminate H || discriminate H0.
 Qed.
 
 Lemma Zsgn_24 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (y <= 0)%Z.
 Proof.
- intros [[| p2| p2]| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *;
+ intros [|p1|p1] [|p2|p2]; simpl in |- *;
   intros H H0; discriminate H || discriminate H0.
 Qed.