Elimination du '

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

3 files changed, 6 insertions, 6 deletions

diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v
index c4ec7baf8d..07da482309 100644
--- a/contrib/omega/Zcomplements.v
+++ b/contrib/omega/Zcomplements.v
@@ -70,8 +70,8 @@ Lemma Zlt_Zmult_right : (x,y,z:Z)`z>0` -> `x < y` -> `x*z < y*z`.
 
 Intros; Rewrite (Zs_pred z); Generalize (Zgt0_le_pred H); Intro;
 Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`;
-[ Simpl; Do 2 '(Rewrite Zmult_n_1); Assumption
-| Unfold Zs; Intros x0 Hx0; Do 6 '(Rewrite Zmult_plus_distr_r);
+[ Simpl; Do 2 (Rewrite Zmult_n_1); Assumption
+| Unfold Zs; Intros x0 Hx0; Do 6 (Rewrite Zmult_plus_distr_r);
   Repeat Rewrite Zmult_n_1;
   Intro; Apply Zlt_Zplus; Assumption
 | Assumption ].
diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v
index 82eeb45737..9e90f63e6a 100644
--- a/contrib/omega/Zpower.v
+++ b/contrib/omega/Zpower.v
@@ -340,7 +340,7 @@ Intros; Apply iter_pos_invariant with
     [ Intro; Rewrite NEG_xI; Unfold Zminus; Intro; Elim H; Intros; Split; 
       [ Rewrite H0; Rewrite Zplus_assoc;
       	Apply f_equal with f:=[z:Z]`z+r`;
-      	Do 2 '(Rewrite Zmult_plus_distr_l);
+      	Do 2 (Rewrite Zmult_plus_distr_l);
        	Rewrite Zmult_assoc; 
       	Rewrite (Zmult_sym (NEG p1) `2`);
       	Rewrite <- Zplus_assoc;
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index 55f3e9bf0c..34cb485fd6 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -8,7 +8,7 @@ Implicit Arguments On.
 
 Lemma index_eq_prop: (n,m:index)(Is_true (index_eq n m)) -> n=m.
 Proof.
-  Induction n; Induction m; Simpl; Try '(Reflexivity Orelse Contradiction).
+  Induction n; Induction m; Simpl; Try (Reflexivity Orelse Contradiction).
   Intros; Rewrite (H i0); Trivial.
   Intros; Rewrite (H i0); Trivial.
 Save.
@@ -845,7 +845,7 @@ Implicit Arguments Off.
 
 Lemma spolynomial_of_ok : (p:polynomial)
   (interp_p p)==(interp_sp Aplus Amult Azero vm (spolynomial_of p)).
-Induction p; Reflexivity Orelse '(Simpl; Intros).
+Induction p; Reflexivity Orelse (Simpl; Intros).
 Rewrite H; Rewrite H0; Reflexivity.
 Rewrite H; Rewrite H0; Reflexivity.
 Rewrite H.
@@ -857,7 +857,7 @@ Save.
 Theorem polynomial_normalize_ok : (p:polynomial)
   (polynomial_normalize p)
   ==(spolynomial_normalize Aplus Amult Aone (spolynomial_of p)).
-Induction p; Reflexivity Orelse '(Simpl; Intros).
+Induction p; Reflexivity Orelse (Simpl; Intros).
 Rewrite H; Rewrite H0; Reflexivity.
 Rewrite H; Rewrite H0; Reflexivity.
 Rewrite H; Simpl.