induction/destruct : nicer syntax for generating equations (solves #2741)

 The ugly syntax "destruct x as [ ]_eqn:H" is replaced by:

  destruct x eqn:H
  destruct x as [ ] eqn:H

 Some with induction. Of course, the pattern behind "as" is arbitrary.
 For an anonymous version, H could be replaced by ?. The old syntax
 with "_eqn" still works for the moment, by triggers a warning.

 For making this new syntax work, we had to change the seldom-used
 "induction x y z using foo" into "induction x, y, z using foo".
 Now, only one "using" can be used per command instead of one per
 comma-separated group earlier, but I doubt this will bother anyone.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15566 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 19 insertions, 19 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index f6801da20..d7dd987fb 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -202,7 +202,7 @@ Lemma nat_compare_spec :
   forall x y, CompareSpec (x=y) (x<y) (y<x) (nat_compare x y).
 Proof.
  intros.
- destruct (nat_compare x y) as [ ]_eqn; constructor.
+ destruct (nat_compare x y) eqn:?; constructor.
  apply nat_compare_eq; auto.
  apply <- nat_compare_lt; auto.
  apply <- nat_compare_gt; auto.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 0c44cfaf1..f779e0772 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -73,7 +73,7 @@ Qed.
 
 Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p.
 Proof.
-  intros; induction n m using nat_double_ind; simpl; auto with arith.
+  intros; induction n, m using nat_double_ind; simpl; auto with arith.
   rewrite <- minus_plus_simpl_l_reverse; auto with arith.
 Qed.
 Hint Resolve mult_minus_distr_r: arith v62.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 9b2a026c2..ad332a947 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -84,13 +84,13 @@ Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)).
 (* Similar variants of destruct *)
 
 Tactic Notation "destruct_with_eqn" constr(x) :=
-  destruct x as []_eqn.
+  destruct x eqn:?.
 Tactic Notation "destruct_with_eqn" ident(n) :=
-  try intros until n; destruct n as []_eqn.
+  try intros until n; destruct n eqn:?.
 Tactic Notation "destruct_with_eqn" ":" ident(H) constr(x) :=
-  destruct x as []_eqn:H.
+  destruct x eqn:H.
 Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) :=
-  try intros until n; destruct n as []_eqn:H.
+  try intros until n; destruct n eqn:H.
 
 (** Break every hypothesis of a certain type *)
 
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index f2b908af0..6778deffa 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -480,7 +480,7 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
  Proof.
   intros (s,Hs) (s',Hs').
   change ({M.Equal s s'}+{~M.Equal s s'}).
-  destruct (M.equal s s') as [ ]_eqn:H; [left|right];
+  destruct (M.equal s s') eqn:H; [left|right];
    rewrite <- M.equal_spec; congruence.
  Defined.
 
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index bcf68f1d4..d9b1fd9bb 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -662,7 +662,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction s; simpl; intros.
   split; intuition; inv.
-  destruct (f a) as [ ]_eqn:F; rewrite !InA_cons, ?IHs; intuition.
+  destruct (f a) eqn:F; rewrite !InA_cons, ?IHs; intuition.
   setoid_replace x with a; auto.
   setoid_replace a with x in F; auto; congruence.
   Qed.
@@ -674,7 +674,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   unfold For_all; induction s; simpl; intros.
   split; intros; auto. inv.
-  destruct (f a) as [ ]_eqn:F.
+  destruct (f a) eqn:F.
   rewrite IHs; auto. firstorder. inv; auto.
   setoid_replace x with a; auto.
   split; intros H'. discriminate.
@@ -688,7 +688,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   unfold Exists; induction s; simpl; intros.
   firstorder. discriminate. inv.
-  destruct (f a) as [ ]_eqn:F.
+  destruct (f a) eqn:F.
   firstorder.
   rewrite IHs; auto.
   firstorder.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 76f09c76e..fd4114cd4 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -396,7 +396,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   induction s; simpl.
   intuition; inv.
   intros.
-  destruct (f a) as [ ]_eqn:E; rewrite ?InA_cons, IHs; intuition.
+  destruct (f a) eqn:E; rewrite ?InA_cons, IHs; intuition.
   setoid_replace x with a; auto.
   setoid_replace a with x in E; auto. congruence.
   Qed.
@@ -420,7 +420,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   unfold For_all; induction s; simpl.
   intuition. inv.
   intros; inv.
-  destruct (f a) as [ ]_eqn:F.
+  destruct (f a) eqn:F.
   rewrite IHs; intuition. inv; auto.
   setoid_replace x with a; auto.
   split; intros H'; try discriminate.
@@ -436,7 +436,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   unfold Exists; induction s; simpl.
   split; [discriminate| intros (x & Hx & _); inv].
   intros.
-  destruct (f a) as [ ]_eqn:F.
+  destruct (f a) eqn:F.
   split; auto.
   exists a; auto.
   rewrite IHs; firstorder.
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index d1c817f54..6b4e154c0 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -416,7 +416,7 @@ Module Make (NN:NType) <: ZType.
  Ltac break_nonneg x px EQx :=
   let H := fresh "H" in
   assert (H:=NN.spec_pos x);
-  destruct (NN.to_Z x) as [|px|px]_eqn:EQx;
+  destruct (NN.to_Z x) as [|px|px] eqn:EQx;
    [clear H|clear H|elim H; reflexivity].
 
  Theorem spec_div_eucl: forall x y,
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index ad7a9f3ae..cabba1131 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -376,7 +376,7 @@ Lemma log_good_step : forall n h1 h2,
   (if n << 2 then 0 else S (h2 (half n))).
 Proof.
 intros n h1 h2 E.
-destruct (n<<2) as [ ]_eqn:H.
+destruct (n<<2) eqn:H.
 auto with *.
 f_equiv. apply E, half_decrease.
 rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H.
diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v
index 7124cd536..695291b8c 100644
--- a/theories/Sorting/Mergesort.v
+++ b/theories/Sorting/Mergesort.v
@@ -131,7 +131,7 @@ Theorem Sorted_merge : forall l1 l2,
   Sorted l1 -> Sorted l2 -> Sorted (merge l1 l2).
 Proof.
 induction l1; induction l2; intros; simpl; auto.
-  destruct (a <=? a0) as ()_eqn:Heq1.
+  destruct (a <=? a0) eqn:Heq1.
     invert H.
       simpl. constructor; trivial; rewrite Heq1; constructor.
       assert (Sorted (merge (b::l) (a0::l2))) by (apply IHl1; auto).
diff --git a/theories/Structures/OrdersAlt.v b/theories/Structures/OrdersAlt.v
index 85e7fb176..5dd917a71 100644
--- a/theories/Structures/OrdersAlt.v
+++ b/theories/Structures/OrdersAlt.v
@@ -140,7 +140,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
  Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
  Proof.
   unfold lt, eq; intros x y z Hxy Hyz.
-  destruct (compare x z) as [ ]_eqn:Hxz; auto.
+  destruct (compare x z) eqn:Hxz; auto.
   rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz.
   rewrite (compare_trans Hxz Hyz) in Hxy; discriminate.
   rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy.
@@ -150,7 +150,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
  Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z.
  Proof.
   unfold lt, eq; intros x y z Hxy Hyz.
-  destruct (compare x z) as [ ]_eqn:Hxz; auto.
+  destruct (compare x z) eqn:Hxz; auto.
   rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy.
   rewrite (compare_trans Hxy Hxz) in Hyz; discriminate.
   rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz.
@@ -169,7 +169,7 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
  Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
  Proof.
   unfold eq, lt, compare; intros.
-  destruct (O.compare x y) as [ ]_eqn:H; auto.
+  destruct (O.compare x y) eqn:H; auto.
   apply CompGt.
   rewrite compare_sym, H; auto.
  Qed.