Parenthèses

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

1 files changed, 3 insertions, 3 deletions

diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 0f641e9b7..dde9daa4c 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.
 
@@ -36,9 +36,9 @@ Theorem eq_nat_decide : (n,m:nat){(eq_nat n m)}+{~(eq_nat n m)}.
 Induction n.
 Destruct m.
 Auto with arith.
-(Intro; Right; Red; Trivial with arith).
+Intro; Right; Red; Trivial with arith.
 Destruct m.
-(Right; Red; Auto with arith).
+Right; Red; Auto with arith.
 Intros.
 Simpl.
 Apply H.