From 2476b8a3397dccc8cadd7422929c844040ecc987 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 22 May 2000 13:05:48 +0000
Subject: Parenthèses

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@457 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Arith/EqNat.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 0f641e9b7a..dde9daa4c3 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.
-- 
cgit v1.2.3