Elimination du '

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

10 files changed, 84 insertions, 84 deletions

diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index ecce3f840..c97a9aaa4 100755
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -24,7 +24,7 @@ Qed.
 Hints Immediate eq_eq_nat : arith v62.
 
 Theorem eq_nat_eq : (n,m:nat)(eq_nat n m)->(n=m).
-Induction n; Induction m; Simpl; '(Contradiction Orelse Auto with arith).
+Induction n; Induction m; Simpl; Contradiction Orelse Auto with arith.
 Qed.
 Hints Immediate eq_nat_eq : arith v62.
 
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index c49c4bf8e..f546a1aa1 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -221,12 +221,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 
@@ -304,7 +304,7 @@ 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);
+  Induction a; Induction b; Simpl; Try (Intro H;Discriminate H);
   Auto with bool.
 Save.
 Hints Resolve andb_prop : bool v62.
@@ -312,7 +312,7 @@ 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);
+  Induction a; Induction b; Simpl; Try (Intro H;Discriminate H);
   Auto with bool.
 Save.
 Hints Resolve andb_prop2 : bool v62.
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index e94bb0ee4..5962e0ed2 100755
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -63,19 +63,19 @@ CoInductive EqSt  : Stream->Stream->Prop :=
 
 Tactic Definition CoInduction proof := 
   Cofix proof; Intros; Constructor;
-    [Clear proof | Try '(Apply proof;Clear proof)].
+    [Clear proof | Try (Apply proof;Clear proof)].
 
 
 (* Extensional equality is an equivalence relation *)
 
 Theorem  EqSt_reflex : (s:Stream)(EqSt s s).
-'(CoInduction EqSt_reflex).
+(CoInduction EqSt_reflex).
 Reflexivity.
 Qed.
 
 Theorem sym_EqSt : 
  (s1:Stream)(s2:Stream)(EqSt s1 s2)->(EqSt s2 s1).
-'(CoInduction Eq_sym).
+(CoInduction Eq_sym).
 Case H;Intros;Symmetry;Assumption.
 Case H;Intros;Assumption.
 Qed.
@@ -83,7 +83,7 @@ Qed.
 
 Theorem trans_EqSt : 
  (s1,s2,s3:Stream)(EqSt s1 s2)->(EqSt s2 s3)->(EqSt s1 s3).
-'(CoInduction Eq_trans).
+(CoInduction Eq_trans).
 Transitivity (hd s2).
 Case H; Intros; Assumption.
 Case H0; Intros; Assumption.
@@ -109,7 +109,7 @@ Qed.
 
 Theorem ntheq_eqst : 
   (s1,s2:Stream)((n:nat)(Str_nth n s1)=(Str_nth n s2))->(EqSt s1 s2).
-'(CoInduction Equiv2).
+(CoInduction Equiv2).
 Apply (H O).
 Intros n; Apply (H (S n)).
 Qed.
@@ -138,7 +138,7 @@ Hypothesis InvThenP   : (x:Stream)(Inv x)->(P x).
 Hypothesis InvIsStable: (x:Stream)(Inv x)->(Inv (tl x)).
 
 Theorem ForAll_coind : (x:Stream)(Inv x)->(ForAll x).
-'(CoInduction ForAll_coind);Auto.
+(CoInduction ForAll_coind);Auto.
 Qed.
 End Co_Induction_ForAll.
 
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index 57e51123d..b886f1211 100755
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -81,7 +81,7 @@ Theorem Couple_as_union:
   (x, y: U) (Union U (Singleton U x) (Singleton U y)) == (Couple U x y).
 Proof.
 Intros x y; Apply Extensionality_Ensembles; Split; Red.
-Intros x0 H'; Elim H'; '(Intros x1 H'0; Elim H'0; Auto with sets).
+Intros x0 H'; Elim H'; (Intros x1 H'0; Elim H'0; Auto with sets).
 Intros x0 H'; Elim H'; Auto with sets.
 Qed.
 
@@ -92,7 +92,7 @@ Theorem Triple_as_union :
 Proof.
 Intros x y z; Apply Extensionality_Ensembles; Split; Red.
 Intros x0 H'; Elim H'.
-Intros x1 H'0; Elim H'0; '(Intros x2 H'1; Elim H'1; Auto with sets).
+Intros x1 H'0; Elim H'0; (Intros x2 H'1; Elim H'1; Auto with sets).
 Intros x1 H'0; Elim H'0; Auto with sets.
 Intros x0 H'; Elim H'; Auto with sets.
 Qed.
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index f7278ba2a..eec50c44f 100755
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -144,7 +144,7 @@ Generalize (H'2 v); Intro h; LApply h;
     [Intro H'14; LApply H'14;
       [Intro h1; Elim h1; Intros z1 h2; Elim h2; Intros H'15 H'16;
         Clear h h0 H'14 h1 h2 | Clear h h0] | Clear h h0] | Clear h]; Auto with sets.
-Red; '(Exists z1; Split); Auto with sets.
+Red; (Exists z1; Split); Auto with sets.
 Apply T with y1; Auto with sets.
 Apply T with t; Auto with sets.
 Qed.
diff --git a/theories/Zarith/Wf_Z.v b/theories/Zarith/Wf_Z.v
index 2be8bf5c1..6b015c77f 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 a9a974f75..8b54415fe 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.
diff --git a/theories/Zarith/auxiliary.v b/theories/Zarith/auxiliary.v
index dbefbc47c..0f0fbc52b 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 aaf27e008..9b6e661fb 100644
--- a/theories/Zarith/fast_integer.v
+++ b/theories/Zarith/fast_integer.v
@@ -155,14 +155,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]);
+(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.
@@ -259,7 +259,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.
@@ -319,18 +319,18 @@ 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 : 
@@ -524,7 +524,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).
@@ -540,8 +540,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:
@@ -673,7 +673,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.
 
@@ -795,7 +795,7 @@ 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 x y;Case x;Case y;Auto with arith);
 Intros p q;Simpl;Case (compare q p EGAL);Auto with arith.
 Save.
 
@@ -804,10 +804,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.
@@ -841,9 +841,9 @@ 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;
+  (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; [
@@ -1114,9 +1114,9 @@ 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;
+  (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
@@ -1167,12 +1167,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
@@ -1183,18 +1183,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).
@@ -1220,7 +1220,7 @@ 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 x y;Case x;Case y;Simpl;Auto with arith);
 Intros;Rewrite <- ZC4;Trivial with arith.
 Save.
 
@@ -1231,10 +1231,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.
@@ -1245,15 +1245,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;
+| 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;
+| 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;
@@ -1261,27 +1261,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;
+| 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);
@@ -1414,7 +1414,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 94404d660..113a59347 100644
--- a/theories/Zarith/zarith_aux.v
+++ b/theories/Zarith/zarith_aux.v
@@ -55,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
@@ -65,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
@@ -117,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 ]
@@ -152,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)); [
@@ -168,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
@@ -204,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 ]
@@ -337,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
@@ -430,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 ].
@@ -438,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 ].
@@ -476,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 ].