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

2 files changed, 2 insertions, 2 deletions

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.