Ajout du langage de tactiques

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

6 files changed, 109 insertions, 104 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index ab1a4b9e04..7737c48378 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -38,7 +38,7 @@ Hints Resolve diff_true_false : bool v62.
 
 Lemma diff_false_true : ~false=true.
 Goal.
-(Red; Intros H; Apply diff_true_false).
+Red; Intros H; Apply diff_true_false.
 Symmetry.
 Assumption.
 Save.
@@ -52,7 +52,7 @@ Hints Resolve eq_true_false_abs : bool.
 Lemma not_true_is_false : (b:bool)~b=true->b=false.
 Destruct b.
 Intros.
-(Red in H; Elim H).
+Red in H; Elim H.
 Reflexivity.
 Intros abs.
 Reflexivity.
@@ -185,13 +185,13 @@ Save.
 Lemma negb_orb : (b1,b2:bool)
   (negb (orb b1 b2)) = (andb (negb b1) (negb b2)).
 Proof.
-  (Destruct b1; Destruct b2; Simpl; Reflexivity).
+  Destruct b1; Destruct b2; Simpl; Reflexivity.
 Qed.
 
 Lemma negb_andb : (b1,b2:bool)
   (negb (andb b1 b2)) = (orb (negb b1) (negb b2)).
 Proof.
-  (Destruct b1; Destruct b2; Simpl; Reflexivity).
+  Destruct b1; Destruct b2; Simpl; Reflexivity.
 Qed.
 
 Lemma negb_sym : (b,b':bool)(b'=(negb b))->(b=(negb b')).
@@ -223,12 +223,12 @@ Save.
 
 Lemma orb_prop : 
   (a,b:bool)(orb a b)=true -> (a = true)\/(b = true).
-Induction a; Induction b; Simpl; Try (Intro H;Discriminate H); Auto with bool.
+Induction a; Induction b; Simpl; Try '(Intro H;Discriminate H); Auto with bool.
 Save.
 
 Lemma orb_prop2 : 
   (a,b:bool)(Is_true (orb a b)) -> (Is_true a)\/(Is_true b).
-Induction a; Induction b; Simpl; Try (Intro H;Discriminate H); Auto with bool.
+Induction a; Induction b; Simpl; Try '(Intro H;Discriminate H); Auto with bool.
 Save.
 
 Lemma orb_true_intro 
@@ -306,14 +306,16 @@ Lemma andb_prop :
   (a,b:bool)(andb a b) = true -> (a = true)/\(b = true).
 
 Proof.
-  Induction a; Induction b; Simpl; Try (Intro H;Discriminate H);Auto with bool.
+  Induction a; Induction b; Simpl; Try '(Intro H;Discriminate H);
+  Auto with bool.
 Save.
 Hints Resolve andb_prop : bool v62.
 
 Lemma andb_prop2 : 
   (a,b:bool)(Is_true (andb a b)) -> (Is_true a)/\(Is_true b).
 Proof.
-  Induction a; Induction b; Simpl; Try (Intro H;Discriminate H); Auto with bool.
+  Induction a; Induction b; Simpl; Try '(Intro H;Discriminate H);
+  Auto with bool.
 Save.
 Hints Resolve andb_prop2 : bool v62.
 
diff --git a/theories/Zarith/Wf_Z.v b/theories/Zarith/Wf_Z.v
index 6b015c77f4..2be8bf5c1a 100644
--- a/theories/Zarith/Wf_Z.v
+++ b/theories/Zarith/Wf_Z.v
@@ -35,7 +35,7 @@ Destruct x; Intros;
   Apply f_equal with f:=POS;
   Apply convert_intro; Auto with arith
 | Absurd `0 <= (NEG p)`;
-  [ Unfold Zle; Simpl; Do 2 (Unfold not); Auto with arith
+  [ Unfold Zle; Simpl; Do 2 '(Unfold not); Auto with arith
   | Assumption]
 ].
 Save.
@@ -61,7 +61,7 @@ Destruct x; Intros;
   Apply f_equal with f:=POS;
   Apply convert_intro; Auto with arith
 | Absurd `0 <= (NEG p)`;
-  [ Unfold Zle; Simpl; Do 2 (Unfold not); Auto with arith
+  [ Unfold Zle; Simpl; Do 2 '(Unfold not); Auto with arith
   | Assumption]
 ].
 Save.
diff --git a/theories/Zarith/Zmisc.v b/theories/Zarith/Zmisc.v
index 28c4cf2084..a9a974f75f 100644
--- a/theories/Zarith/Zmisc.v
+++ b/theories/Zarith/Zmisc.v
@@ -210,9 +210,9 @@ Proof.
   Intro z. Case z;
   [ Left; Compute; Trivial
   | Intro p; Case p; Intros; 
-    (Right; Compute; Exact I) Orelse (Left; Compute; Exact I)
+    '(Right; Compute; Exact I) Orelse '(Left; Compute; Exact I)
   | Intro p; Case p; Intros; 
-    (Right; Compute; Exact I) Orelse (Left; Compute; Exact I) ].
+    '(Right; Compute; Exact I) Orelse '(Left; Compute; Exact I) ].
   (*** was 
   Realizer Zeven_bool.
   Repeat Program; Compute; Trivial.
@@ -224,9 +224,9 @@ Proof.
   Intro z. Case z;
   [ Left; Compute; Trivial
   | Intro p; Case p; Intros; 
-    (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) 
+    '(Left; Compute; Exact I) Orelse '(Right; Compute; Trivial) 
   | Intro p; Case p; Intros; 
-    (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ].
+    '(Left; Compute; Exact I) Orelse '(Right; Compute; Trivial) ].
   (*** was 
   Realizer Zeven_bool.
   Repeat Program; Compute; Trivial.
@@ -238,9 +238,9 @@ Proof.
   Intro z. Case z;
   [ Right; Compute; Trivial
   | Intro p; Case p; Intros; 
-    (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) 
+    '(Left; Compute; Exact I) Orelse '(Right; Compute; Trivial) 
   | Intro p; Case p; Intros; 
-    (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ].
+    '(Left; Compute; Exact I) Orelse '(Right; Compute; Trivial) ].
   (*** was 
   Realizer Zodd_bool.
   Repeat Program; Compute; Trivial.
@@ -281,21 +281,21 @@ Lemma Zeven_div2 : (x:Z) (Zeven x) -> `x = 2*(Zdiv2 x)`.
 Proof.
 Destruct x.
 Auto with arith.
-(Destruct p; Auto with arith).
-Intros. (Absurd (Zeven (POS (xI p0))); Red; Auto with arith).
-Intros. (Absurd (Zeven `1`); Red; Auto with arith).
-(Destruct p; Auto with arith).
-Intros. (Absurd (Zeven (NEG (xI p0))); Red; Auto with arith).
-Intros. (Absurd (Zeven `-1`); Red; Auto with arith).
+Destruct p; Auto with arith.
+Intros. Absurd (Zeven (POS (xI p0))); Red; Auto with arith.
+Intros. Absurd (Zeven `1`); Red; Auto with arith.
+Destruct p; Auto with arith.
+Intros. Absurd (Zeven (NEG (xI p0))); Red; Auto with arith.
+Intros. Absurd (Zeven `-1`); Red; Auto with arith.
 Save.
 
 Lemma Zodd_div2 : (x:Z) `x >= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)+1`.
 Proof.
 Destruct x.
-Intros. (Absurd (Zodd `0`); Red; Auto with arith).
-(Destruct p; Auto with arith).
-Intros. (Absurd (Zodd (POS (xO p0))); Red; Auto with arith).
-Intros. (Absurd `(NEG p) >= 0`; Red; Auto with arith).
+Intros. Absurd (Zodd `0`); Red; Auto with arith.
+Destruct p; Auto with arith.
+Intros. Absurd (Zodd (POS (xO p0))); Red; Auto with arith.
+Intros. Absurd `(NEG p) >= 0`; Red; Auto with arith.
 Save.
 
 Lemma Z_modulo_2 : (x:Z) `x >= 0` -> { y:Z | `x=2*y` }+{ y:Z | `x=2*y+1` }.
@@ -344,7 +344,7 @@ Apply rename with x:=`x ?= y`; Intro r; Elim r;
 Save.
 
 Lemma Zcompare_x_x : (x:Z) `x ?= x` = EGAL.
-(Intro; Apply Case (Zcompare_EGAL x x) of [h1,h2: ?]h2 end).
+Intro; Apply Case (Zcompare_EGAL x x) of [h1,h2: ?]h2 end.
 Apply refl_equal.
 Save.
 
diff --git a/theories/Zarith/auxiliary.v b/theories/Zarith/auxiliary.v
index bee3e0a234..e9678721b9 100644
--- a/theories/Zarith/auxiliary.v
+++ b/theories/Zarith/auxiliary.v
@@ -564,7 +564,7 @@ Theorem OMEGA10:(v,c1,c2,l1,l2,k1,k2:Z)
   = (Zplus (Zmult v (Zplus (Zmult c1 k1) (Zmult c2 k2)))
            (Zplus (Zmult l1 k1) (Zmult l2 k2))).
 
-Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
+Intros; Repeat '(Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
 Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; 
 Rewrite (Zplus_permute (Zmult l1 k1) (Zmult (Zmult v c2) k2)); Trivial with arith.
 Save.
@@ -573,7 +573,7 @@ Theorem OMEGA11:(v1,c1,l1,l2,k1:Z)
   (Zplus (Zmult (Zplus (Zmult v1 c1) l1) k1) l2)
   = (Zplus (Zmult v1 (Zmult c1 k1)) (Zplus (Zmult l1 k1) l2)).
 
-Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
+Intros; Repeat '(Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
 Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Trivial with arith.
 Save.
 
@@ -581,7 +581,7 @@ Theorem OMEGA12:(v2,c2,l1,l2,k2:Z)
   (Zplus l1 (Zmult (Zplus (Zmult v2 c2) l2) k2))
   = (Zplus (Zmult v2 (Zmult c2 k2)) (Zplus l1 (Zmult l2 k2))).
 
-Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
+Intros; Repeat '(Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
 Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Rewrite Zplus_permute;
 Trivial with arith.
 Save.
@@ -610,7 +610,7 @@ Theorem OMEGA15:(v,c1,c2,l1,l2,k2:Z)
   = (Zplus (Zmult v (Zplus c1  (Zmult c2 k2)))
            (Zplus l1 (Zmult l2 k2))).
 
-Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
+Intros; Repeat '(Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
 Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; 
 Rewrite (Zplus_permute l1 (Zmult (Zmult v c2) k2)); Trivial with arith.
 Save.
@@ -619,7 +619,7 @@ Theorem OMEGA16:
   (v,c,l,k:Z)
    (Zmult (Zplus (Zmult v c) l) k) = (Zplus (Zmult v (Zmult c k)) (Zmult l k)).
 
-Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
+Intros; Repeat '(Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r);
 Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Trivial with arith.
 Save.
 
diff --git a/theories/Zarith/fast_integer.v b/theories/Zarith/fast_integer.v
index 93b78f9e44..5d955f5eed 100644
--- a/theories/Zarith/fast_integer.v
+++ b/theories/Zarith/fast_integer.v
@@ -154,14 +154,14 @@ Definition sub_un := [x:positive]
 
 Lemma sub_add_one : (x:positive) (sub_un (add_un x)) = x.
 Proof.
-(Induction x; [Idtac | Idtac | Simpl;Auto with arith ]); 
-(Intros p; Elim p; [Idtac | Idtac | Simpl;Auto with arith ]);
-(Simpl; Intros q H1 H2; Case H2; Simpl; Trivial with arith).
+'(Induction x; [Idtac | Idtac | Simpl;Auto with arith ]);
+'(Intros p; Elim p; [Idtac | Idtac | Simpl;Auto with arith]);
+Simpl; Intros q H1 H2; Case H2; Simpl; Trivial with arith.
 Save.
 
 Lemma is_double_moins_un : (x:positive) (add_un (double_moins_un x)) = (xO x).
 Proof.
-(Induction x;Simpl;Auto with arith); (Intros m H;Rewrite H;Trivial with arith).
+'(Induction x;Simpl;Auto with arith); Intros m H;Rewrite H;Trivial with arith.
 Save.
 
 Lemma add_sub_one : (x:positive) (x=xH) \/ (add_un (sub_un x)) = x.
@@ -258,7 +258,7 @@ Theorem compare_convert1 :
   ~(compare x y SUPERIEUR) = EGAL /\ ~(compare x y INFERIEUR) = EGAL.
 Proof.
 Induction x;Induction y;Split;Simpl;Auto with arith;
-  (Discriminate Orelse (Elim (H p0); Auto with arith)).
+  Discriminate Orelse '(Elim (H p0); Auto with arith).
 Save.
 
 Theorem compare_convert_EGAL : (x,y:positive) (compare x y EGAL) = EGAL -> x=y.
@@ -303,7 +303,7 @@ Lemma ZLSI:
                 (compare x y EGAL) = INFERIEUR.
 Proof.
 Induction x;Induction y;Simpl;Auto with arith; 
-  (Discriminate Orelse Intros H;Discriminate H).
+  Discriminate Orelse Intros H;Discriminate H.
 Save.
 
 Lemma ZLIS:
@@ -311,23 +311,25 @@ Lemma ZLIS:
                 (compare x y EGAL) = SUPERIEUR.
 Proof.
 Induction x;Induction y;Simpl;Auto with arith; 
-  (Discriminate Orelse Intros H;Discriminate H).
+  Discriminate Orelse Intros H;Discriminate H.
 Save.
 
 Lemma ZLII:
  (x,y:positive) (compare x y INFERIEUR) = INFERIEUR ->
                 (compare x y EGAL) = INFERIEUR \/ x = y.
 Proof.
-(Induction x;Induction y;Simpl;Auto with arith;Try Discriminate);
-  (Intros z H1 H2; Elim (H z H2);Auto with arith; Intros E;Rewrite E;Auto with arith).
+'(Induction x;Induction y;Simpl;Auto with arith;Try Discriminate);
+  Intros z H1 H2; Elim (H z H2);Auto with arith; Intros E;Rewrite E;
+  Auto with arith.
 Save.
 
 Lemma ZLSS:
  (x,y:positive) (compare x y SUPERIEUR) = SUPERIEUR ->
                 (compare x y EGAL) = SUPERIEUR \/ x = y.
 Proof.
-(Induction x;Induction y;Simpl;Auto with arith;Try Discriminate);
-  (Intros z H1 H2; Elim (H z H2);Auto with arith; Intros E;Rewrite E;Auto with arith).
+'(Induction x;Induction y;Simpl;Auto with arith;Try Discriminate);
+  Intros z H1 H2; Elim (H z H2);Auto with arith; Intros E;Rewrite E;
+  Auto with arith.
 Save.
 
 Theorem compare_convert_INFERIEUR : 
@@ -521,7 +523,7 @@ Save.
 
 Lemma ZL11: (x:positive) (x=xH) \/ ~(x=xH).
 Proof.
-Intros x;Case x;Intros; ((Left;Reflexivity) Orelse (Right;Discriminate)).
+Intros x;Case x;Intros; '(Left;Reflexivity) Orelse '(Right;Discriminate).
 Save.
 
 Lemma ZL12: (q:positive) (add_un q) = (add q xH).
@@ -537,7 +539,8 @@ Save.
 Theorem ZL13:
   (x,y:positive)(add_carry x y) = (add_un (add x y)).
 Proof.
-(Induction x;Induction y;Simpl;Auto with arith); (Intros q H1;Rewrite H;Auto with arith).
+'(Induction x;Induction y;Simpl;Auto with arith); Intros q H1;Rewrite H;
+  Auto with arith.
 Save.
 
 Theorem ZL14:
@@ -669,7 +672,7 @@ Definition Op := [r:relation]
 
 Lemma ZC4: (x,y:positive) (compare x y EGAL) = (Op (compare y x EGAL)).
 Proof.
-(((Intros x y;Elim (Dcompare (compare y x EGAL));[Idtac | Intros H;Elim H]);
+'('('(Intros x y;Elim (Dcompare (compare y x EGAL));[Idtac | Intros H;Elim H]);
 Intros E;Rewrite E;Simpl); [Apply ZC3 | Apply ZC2 | Apply ZC1 ]); Assumption.
 Save.
 
@@ -791,8 +794,8 @@ Save.
 Theorem Zopp_Zplus: 
   (x,y:Z) (Zopp (Zplus x y)) = (Zplus (Zopp x) (Zopp y)).
 Proof.
-(Intros x y;Case x;Case y;Auto with arith);
-(Intros p q;Simpl;Case (compare q p EGAL);Auto with arith).
+'(Intros x y;Case x;Case y;Auto with arith);
+Intros p q;Simpl;Case (compare q p EGAL);Auto with arith.
 Save.
 
 Theorem Zplus_sym: (x,y:Z) (Zplus x y) = (Zplus y x).
@@ -800,10 +803,10 @@ Proof.
 Induction x;Induction y;Simpl;Auto with arith; [
   Intros q;Rewrite add_sym;Auto with arith
 | Intros q; Rewrite (ZC4 q p);
-  (Elim (Dcompare (compare p q EGAL));[Idtac|Intros H;Elim H]);
+  '(Elim (Dcompare (compare p q EGAL));[Idtac|Intros H;Elim H]);
   Intros E;Rewrite E;Auto with arith
 | Intros q; Rewrite (ZC4 q p);
-  (Elim (Dcompare (compare p q EGAL));[Idtac|Intros H;Elim H]);
+  '(Elim (Dcompare (compare p q EGAL));[Idtac|Intros H;Elim H]);
   Intros E;Rewrite E;Auto with arith
 | Intros q;Rewrite add_sym;Auto with arith ].
 Save.
@@ -837,10 +840,10 @@ Intros x y z';Case z'; [
   Auto with arith
 | Intros z;Simpl; Rewrite add_assoc;Auto with arith
 | Intros z; Simpl;
-  (Elim (Dcompare (compare y z EGAL));[Idtac|Intros H;Elim H;Clear  H]);
+  '(Elim (Dcompare (compare y z EGAL));[Idtac|Intros H;Elim H;Clear  H]);
   Intros E0;Rewrite E0;
-  (Elim (Dcompare (compare (add x y) z EGAL));[Idtac|Intros H;Elim H;Clear H]);
-  Intros E1;Rewrite E1; [
+  '(Elim (Dcompare (compare (add x y) z EGAL));[Idtac|Intros H;Elim H;
+    Clear H]);Intros E1;Rewrite E1; [
     Absurd (compare (add x y) z EGAL)=EGAL; [    (* Cas 1 *)
       Rewrite convert_compare_SUPERIEUR; [
         Discriminate
@@ -1110,10 +1113,10 @@ Theorem weak_Zmult_plus_distr_r:
    (Zmult (POS x) (Zplus y z)) = (Zplus (Zmult (POS x) y) (Zmult (POS x) z)).
 Proof.
 Intros x y' z';Case y';Case z';Auto with arith;Intros y z;
-  (Simpl; Rewrite times_add_distr; Trivial with arith)
+  '(Simpl; Rewrite times_add_distr; Trivial with arith)
 Orelse
- (Simpl; (Elim (Dcompare (compare z y EGAL));[Idtac|Intros H;Elim H;Clear  H]);
-  Intros E0;Rewrite E0; [
+ '(Simpl; '(Elim (Dcompare (compare z y EGAL));[Idtac|Intros H;Elim H;
+   Clear  H]);Intros E0;Rewrite E0; [
     Rewrite (compare_convert_EGAL z y E0);
     Rewrite (convert_compare_EGAL (times x y)); Trivial with arith
   | Cut (compare (times x z) (times x y) EGAL)=INFERIEUR; [
@@ -1163,12 +1166,12 @@ Definition Zcompare := [x,y:Z]
 Theorem Zcompare_EGAL : (x,y:Z) (Zcompare x y) = EGAL <-> x = y.
 Proof.
 Intros x y;Split; [
-  Case x;Case y;Simpl;Auto with arith; Try (Intros;Discriminate H); [
+  Case x;Case y;Simpl;Auto with arith; Try '(Intros;Discriminate H); [
     Intros x' y' H; Rewrite (compare_convert_EGAL y' x' H); Trivial with arith
   | Intros x' y' H; Rewrite (compare_convert_EGAL y' x'); [
       Trivial with arith
     | Generalize H; Case (compare y' x' EGAL);
-      (Trivial with arith Orelse (Intros C;Discriminate C))]]
+      Trivial with arith Orelse '(Intros C;Discriminate C)]]
 | Intros E;Rewrite E; Case y; [
     Trivial with arith
   | Simpl;Exact convert_compare_EGAL
@@ -1179,18 +1182,18 @@ Theorem Zcompare_ANTISYM :
   (x,y:Z) (Zcompare x y) = SUPERIEUR <->  (Zcompare y x) = INFERIEUR.
 Proof.
 Intros x y;Split; [
-  Case x;Case y;Simpl;Intros;(
-    Trivial with arith Orelse Discriminate H Orelse (Apply ZC1; Assumption) Orelse
-    (Cut (compare p p0 EGAL)=SUPERIEUR; [
+  Case x;Case y;Simpl;Intros;'(
+    Trivial with arith Orelse Discriminate H Orelse '(Apply ZC1; Assumption) Orelse
+    '(Cut (compare p p0 EGAL)=SUPERIEUR; [
        Intros H1;Rewrite H1;Auto with arith
      | Apply ZC2; Generalize H ; Case (compare p0 p EGAL);
-       (Trivial with arith Orelse (Intros H2;Discriminate H2))]))
-| Case x;Case y;Simpl;Intros;(
-    Trivial with arith Orelse Discriminate H Orelse (Apply ZC2; Assumption) Orelse
-    (Cut (compare p0 p EGAL)=INFERIEUR; [
+       Trivial with arith Orelse '(Intros H2;Discriminate H2)]))
+| Case x;Case y;Simpl;Intros;'(
+    Trivial with arith Orelse Discriminate H Orelse '(Apply ZC2; Assumption) Orelse
+    '(Cut (compare p0 p EGAL)=INFERIEUR; [
        Intros H1;Rewrite H1;Auto with arith
      | Apply ZC1; Generalize H ; Case (compare p p0 EGAL);
-       (Trivial with arith Orelse (Intros H2;Discriminate H2))]))].
+       Trivial with arith Orelse '(Intros H2;Discriminate H2)]))].
 Save.
 
 Theorem le_minus: (i,h:nat) (le (minus i h) i).
@@ -1216,8 +1219,8 @@ Save.
 Theorem Zcompare_Zopp :
   (x,y:Z) (Zcompare x y) = (Zcompare (Zopp y) (Zopp x)).
 Proof.
-(Intros x y;Case x;Case y;Simpl;Auto with arith);
-(Intros;Rewrite <- ZC4;Trivial with arith).
+'(Intros x y;Case x;Case y;Simpl;Auto with arith);
+Intros;Rewrite <- ZC4;Trivial with arith.
 Save.
 
 Hints Resolve convert_compare_EGAL.
@@ -1227,10 +1230,10 @@ Theorem weaken_Zcompare_Zplus_compatible :
     (Zcompare (Zplus (POS z) x) (Zplus (POS z) y)) = (Zcompare x y)) ->
    (x,y,z:Z) (Zcompare (Zplus z x) (Zplus z y)) = (Zcompare x y).
 Proof.
-(Intros H x y z;Case x;Case y;Case z;Auto with arith;
-Try (Intros; Rewrite Zcompare_Zopp; Do 2 Rewrite Zopp_Zplus;
+'(Intros H x y z;Case x;Case y;Case z;Auto with arith;
+Try '(Intros; Rewrite Zcompare_Zopp; Do 2 Rewrite Zopp_Zplus;
      Rewrite Zopp_NEG; Rewrite H; Simpl; Auto with arith));
-Try (Intros; Simpl; Rewrite <- ZC4; Auto with arith).
+Try '(Intros; Simpl; Rewrite <- ZC4; Auto with arith).
 Save.
 
 Hints Resolve ZC4.
@@ -1241,14 +1244,15 @@ Theorem weak_Zcompare_Zplus_compatible :
 Proof.
 Intros x y z;Case x;Case y;Simpl;Auto with arith; [
   Intros p;Apply convert_compare_INFERIEUR; Apply ZL17
-| Intros p;(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H;Clear H]);
-  Intros E;Rewrite E;Auto with arith; Apply convert_compare_SUPERIEUR;
-  Rewrite true_sub_convert; [ Unfold gt ;Apply ZL16 | Assumption ]
-| Intros p;(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H;Clear H]);
-  Intros E;Auto with arith; Apply convert_compare_SUPERIEUR;Unfold gt;
-  Apply ZL17
+| Intros p;'(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H;
+  Clear H]);Intros E;Rewrite E;Auto with arith;
+  Apply convert_compare_SUPERIEUR; Rewrite true_sub_convert; [ Unfold gt ;
+  Apply ZL16 | Assumption ]
+| Intros p;'(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H;
+  Clear H]);Intros E;Auto with arith; Apply convert_compare_SUPERIEUR;
+  Unfold gt;Apply ZL17
 | Intros p q;
-  (Elim (Dcompare (compare q p EGAL));[Idtac|Intros H;Elim H;Clear  H]);
+  '(Elim (Dcompare (compare q p EGAL));[Idtac|Intros H;Elim H;Clear  H]);
   Intros E;Rewrite E;[
     Rewrite (compare_convert_EGAL q p E); Apply convert_compare_EGAL
   | Apply convert_compare_INFERIEUR;Do 2 Rewrite convert_add;Apply lt_reg_l;
@@ -1256,26 +1260,27 @@ Intros x y z;Case x;Case y;Simpl;Auto with arith; [
   | Apply convert_compare_SUPERIEUR;Unfold gt ;Do 2 Rewrite convert_add;
     Apply lt_reg_l;Exact (compare_convert_SUPERIEUR q p E) ]
 | Intros p q; 
-  (Elim (Dcompare (compare z p EGAL));[Idtac|Intros H;Elim H;Clear  H]);
+  '(Elim (Dcompare (compare z p EGAL));[Idtac|Intros H;Elim H;Clear  H]);
   Intros E;Rewrite E;Auto with arith;
   Apply convert_compare_SUPERIEUR; Rewrite true_sub_convert; [
     Unfold gt; Apply lt_trans with m:=(convert z); [Apply ZL16 | Apply ZL17]
   | Assumption ]
-| Intros p;(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H;Clear H]);
-  Intros E;Rewrite E;Auto with arith; Simpl; Apply convert_compare_INFERIEUR;
-  Rewrite true_sub_convert;[Apply ZL16|Assumption]
+| Intros p;'(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H;
+  Clear H]);Intros E;Rewrite E;Auto with arith; Simpl;
+  Apply convert_compare_INFERIEUR;Rewrite true_sub_convert;[Apply ZL16|
+  Assumption]
 | Intros p q;
-  (Elim (Dcompare (compare z q EGAL));[Idtac|Intros H;Elim H;Clear  H]);
+  '(Elim (Dcompare (compare z q EGAL));[Idtac|Intros H;Elim H;Clear  H]);
   Intros E;Rewrite E;Auto with arith; Simpl;Apply convert_compare_INFERIEUR;
   Rewrite true_sub_convert;[
     Apply lt_trans with m:=(convert z) ;[Apply ZL16|Apply ZL17]
   | Assumption]
 | Intros p q;
-  (Elim (Dcompare (compare z q EGAL));[Idtac|Intros H;Elim H;Clear  H]);
+  '(Elim (Dcompare (compare z q EGAL));[Idtac|Intros H;Elim H;Clear  H]);
   Intros E0;Rewrite E0;
-  (Elim (Dcompare (compare z p EGAL));[Idtac|Intros H;Elim H;Clear  H]);
+  '(Elim (Dcompare (compare z p EGAL));[Idtac|Intros H;Elim H;Clear  H]);
   Intros E1;Rewrite E1;
-  (Elim (Dcompare (compare q p EGAL));[Idtac|Intros H;Elim H;Clear  H]);
+  '(Elim (Dcompare (compare q p EGAL));[Idtac|Intros H;Elim H;Clear  H]);
   Intros E2;Rewrite E2;Auto with arith; [
     Absurd (compare q p EGAL)=INFERIEUR; [
       Rewrite <- (compare_convert_EGAL z q E0);
@@ -1408,7 +1413,7 @@ Theorem Zcompare_trans_SUPERIEUR :
             (Zcompare x z) = SUPERIEUR.
 Proof.
 Intros x y z;Case x;Case y;Case z; Simpl;
-Try (Intros; Discriminate H Orelse Discriminate H0);
+Try '(Intros; Discriminate H Orelse Discriminate H0);
 Auto with arith; [
   Intros p q r H H0;Apply convert_compare_SUPERIEUR; Unfold gt;
   Apply lt_trans with m:=(convert q);
diff --git a/theories/Zarith/zarith_aux.v b/theories/Zarith/zarith_aux.v
index 8b8be64acb..94404d6602 100644
--- a/theories/Zarith/zarith_aux.v
+++ b/theories/Zarith/zarith_aux.v
@@ -11,13 +11,11 @@
 Require Arith.
 Require Export fast_integer.
 
-Tactic Definition ElimCompare [$com1 $com2] :=
-  [ < : tactic : <  
-       Elim (Dcompare (Zcompare $com1 $com2)); [
+Tactic Definition ElimCompare com1 com2:=
+  Elim (Dcompare (Zcompare com1 com2)); [
          Idtac 
        | Intro hidden_auxiliary; Elim hidden_auxiliary; 
-         Clear hidden_auxiliary ] >>].
-
+         Clear hidden_auxiliary ].
 
 Definition Zlt := [x,y:Z](Zcompare x y) = INFERIEUR.
 Definition Zgt := [x,y:Z](Zcompare x y) = SUPERIEUR.
@@ -57,7 +55,7 @@ Save.
 
 Theorem Zle_gt_trans : (n,m,p:Z)(Zle m n)->(Zgt m p)->(Zgt n p).
 
-Unfold Zle Zgt; Intros n m p H1 H2; ElimCompare m n; [
+Unfold Zle Zgt; Intros n m p H1 H2; '(ElimCompare m n); [
   Intro E; Elim (Zcompare_EGAL m n); Intros H3 H4;Rewrite <- (H3 E); Assumption
 | Intro H3; Apply Zcompare_trans_SUPERIEUR with y:=m;[
     Elim (Zcompare_ANTISYM n m); Intros H4 H5;Apply H5; Assumption
@@ -67,7 +65,7 @@ Save.
 
 Theorem Zgt_le_trans : (n,m,p:Z)(Zgt n m)->(Zle p m)->(Zgt n p).
 
-Unfold Zle Zgt ;Intros n m p H1 H2; ElimCompare p m; [
+Unfold Zle Zgt ;Intros n m p H1 H2; '(ElimCompare p m); [
   Intros E;Elim (Zcompare_EGAL p m);Intros H3 H4; Rewrite (H3 E); Assumption
 | Intro H3; Apply Zcompare_trans_SUPERIEUR with y:=m; [
     Assumption
@@ -119,7 +117,7 @@ Save.
 
 Lemma Zle_gt_S       : (n,p:Z)(Zle n p)->(Zgt (Zs p) n).
 
-Unfold Zle Zgt ;Intros n p H; ElimCompare n p; [
+Unfold Zle Zgt ;Intros n p H; '(ElimCompare n p); [
   Intros H1;Elim (Zcompare_EGAL n p);Intros H2 H3; Rewrite <- H2; [
     Exact (Zgt_Sn_n n)
   | Assumption ]
@@ -154,7 +152,7 @@ Theorem Zcompare_et_un:
     ~(Zcompare x (Zplus y (POS xH)))=INFERIEUR.
 
 Intros x y; Split; [
-  Intro H; ElimCompare x (Zplus y (POS xH));[
+  Intro H; '(ElimCompare x (Zplus y (POS xH)));[
     Intro H1; Rewrite H1; Discriminate
   | Intros H1; Elim SUPERIEUR_POS with 1:=H; Intros h H2; 
     Absurd (gt (convert h) O) /\ (lt (convert h) (S O)); [
@@ -170,7 +168,7 @@ Intros x y; Split; [
         Rewrite (Zplus_sym x);Rewrite Zplus_assoc; Rewrite Zplus_inverse_r;
         Simpl; Exact H1 ]]
   | Intros H1;Rewrite -> H1;Discriminate ]
-| Intros H; ElimCompare x (Zplus y (POS xH)); [
+| Intros H; '(ElimCompare x (Zplus y (POS xH))); [
     Intros H1;Elim (Zcompare_EGAL x (Zplus y (POS xH))); Intros H2 H3;
     Rewrite  (H2 H1); Exact (Zgt_Sn_n y)
   | Intros H1;Absurd (Zcompare x (Zplus y (POS xH)))=INFERIEUR;Assumption
@@ -206,7 +204,7 @@ Save.
 
 Theorem Zgt_S        : (n,m:Z)(Zgt (Zs n) m)->((Zgt n m)\/(<Z>m=n)).
 
-Intros n m H; Unfold Zgt; ElimCompare n m; [
+Intros n m H; Unfold Zgt; '(ElimCompare n m); [
   Elim (Zcompare_EGAL n m); Intros H1 H2 H3;Rewrite -> H1;Auto with arith
 | Intros H1;Absurd (Zcompare m n)=SUPERIEUR; 
     [ Exact (Zgt_S_le m n H) | Elim (Zcompare_ANTISYM m n); Auto with arith ]
@@ -339,7 +337,7 @@ Save.
 
 Theorem Zle_antisym : (n,m:Z)(Zle n m)->(Zle m n)->(n=m).
 
-Unfold Zle ;Intros n m H1 H2; ElimCompare n m; [
+Unfold Zle ;Intros n m H1 H2; '(ElimCompare n m); [
   Elim (Zcompare_EGAL n m);Auto with arith
 | Intros H3;Absurd (Zcompare m n)=SUPERIEUR; [
     Assumption
@@ -432,7 +430,7 @@ Save.
  
 Theorem Zle_lt_or_eq : (n,m:Z)(Zle n m)->((Zlt n m) \/ n=m).
 
-Unfold Zle Zlt ;Intros n m H; ElimCompare n m; [
+Unfold Zle Zlt ;Intros n m H; '(ElimCompare n m); [
   Elim (Zcompare_EGAL n m);Auto with arith
 | Auto with arith
 | Intros H';Absurd (Zcompare n m)=SUPERIEUR;Assumption ].
@@ -440,7 +438,7 @@ Save.
 
 Theorem Zle_or_lt : (n,m:Z)((Zle n m)\/(Zlt m n)).
 
-Unfold Zle Zlt ;Intros n m; ElimCompare n m; [
+Unfold Zle Zlt ;Intros n m; '(ElimCompare n m); [
   Intros E;Rewrite -> E;Left;Discriminate
 | Intros E;Rewrite -> E;Left;Discriminate
 | Elim (Zcompare_ANTISYM n m); Auto with arith ].
@@ -478,18 +476,18 @@ Definition Zmin := [n,m:Z]
 Lemma Zmin_SS : (n,m:Z)((Zs (Zmin n m))=(Zmin (Zs n) (Zs m))).
 
 Intros n m;Unfold Zmin; Rewrite (Zcompare_n_S n m);
-ElimCompare n m;Intros E;Rewrite E;Auto with arith.
+'(ElimCompare n m);Intros E;Rewrite E;Auto with arith.
 Save.
 
 Lemma Zle_min_l : (n,m:Z)(Zle (Zmin n m) n).
 
-Intros n m;Unfold Zmin ; ElimCompare n m;Intros E;Rewrite -> E;
+Intros n m;Unfold Zmin ; '(ElimCompare n m);Intros E;Rewrite -> E;
   [ Apply Zle_n | Apply Zle_n | Apply Zlt_le_weak; Apply Zgt_lt;Exact E ].
 Save.
 
 Lemma Zle_min_r : (n,m:Z)(Zle (Zmin n m) m).
 
-Intros n m;Unfold Zmin ;ElimCompare n m;Intros E;Rewrite -> E;[
+Intros n m;Unfold Zmin ;'(ElimCompare n m);Intros E;Rewrite -> E;[
   Unfold Zle ;Rewrite -> E;Discriminate
 | Unfold Zle ;Rewrite -> E;Discriminate
 | Apply Zle_n ].