Double Induction prend maintenant des noms d'hyppthèses

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

5 files changed, 7 insertions, 6 deletions

diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 587351c375..b4a232e204 100755
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -64,7 +64,7 @@ Qed.
 
 Definition beq_nat_eq : (x,y:nat)true=(beq_nat x y)->x=y.
 Proof.
-  Double Induction 1 2; Simpl.
+  Double Induction x y; Simpl.
     Reflexivity.
     Intros; Discriminate H0.
     Intros; Discriminate H0.
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index fd243969bc..d21fde297f 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -1211,7 +1211,7 @@ Qed.
 Hints Resolve pos_INR: real.
 
 Lemma INR_lt:(n,m:nat)``(INR n) < (INR m)``->(lt n m).
-Double Induction 1 2;Intros.
+Double Induction n m;Intros.
 Simpl;ElimType False;Apply (Rlt_antirefl R0);Auto.
 Auto with arith.
 Generalize (pos_INR (S n0));Intro;Cut (INR O)==R0;
@@ -1584,4 +1584,5 @@ Qed.
 
 Lemma add_auto : (p,q:nat) ``(INR2 (S p))+(INR2 q)==(INR2 p)+(INR2 (S q))``.
 Intros; Repeat Rewrite <- INR_eq_INR2; Repeat Rewrite S_INR; Ring.
-Qed.
\ No newline at end of file
+Qed.
+
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 7bb1236adb..e0e04d8224 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -40,7 +40,7 @@ Cut ~(plus n0 (1))=O.
 Intro;Apply H;Assumption.
 Replace (plus n0 (1)) with (S n0);[Auto|Ring].
 Intros;Ring.
-Double Induction 1 2;Simpl;Auto.
+Double Induction n m;Simpl;Auto.
 Qed.
 
 (*********)
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index c88cdfaf20..68e77d5289 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -64,7 +64,7 @@ Qed.
 
 (*********)
 Lemma growing_prop:(n,m:nat)Un_growing->(ge n m)->(Rge (Un n) (Un m)).
-Double Induction 1 2;Intros.
+Double Induction n m;Intros.
 Unfold Rge;Right;Trivial.
 ElimType False;Unfold ge in H1;Generalize (le_Sn_O n0);Intro;Auto.
 Cut (ge n0 (0)).
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index dcd8f941ce..4f0dc8c73c 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -61,7 +61,7 @@ with rexpr0 : constr :=
 
 with meta : ast :=
 | rimpl [ "?" ] -> [ (ISEVAR) ]
-| rmeta [ "?" prim:number($n) ] -> [ (META $n) ]
+| rmeta [ "?" prim:numarg($n) ] -> [ (META $n) ]
 
 with rapplication : constr :=
   apply [ rapplication($p) rexpr($c1) ] -> [ ($p $c1) ]