From daa75d5ffb8dfdf414bed31fbfe1e91718d6a5dc Mon Sep 17 00:00:00 2001
From: mohring
Date: Thu, 26 Oct 2000 12:32:18 +0000
Subject: Retire les parentheses autour des tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@766 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Relations/Operators_Properties.v | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 99b9eb715c..e3da5130f7 100755
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -45,15 +45,15 @@ Save.
 Intros.
 Generalize H H0 .
 Clear  H H0.
-(Elim H1; Intros; Auto with sets).
-(Apply H2 with x; Auto with sets).
+Elim H1; Intros; Auto with sets.
+Apply H2 with x; Auto with sets.
 
 Apply H3.
-(Apply H0; Auto with sets).
+Apply H0; Auto with sets.
 
 Intros.
-(Apply H5 with P0; Auto with sets).
-(Apply rt_trans with y; Auto with sets).
+Apply H5 with P0; Auto with sets.
+Apply rt_trans with y; Auto with sets.
 Save.
 
 
@@ -65,9 +65,9 @@ Section Clos_Refl_Sym_Trans.
   Lemma clos_rt_clos_rst: (inclusion A (clos_refl_trans A R)
 				        (clos_refl_sym_trans A R)).
 Red.
-(Induction 1; Auto with sets).
+Induction 1; Auto with sets.
 Intros.
-(Apply rst_trans with y0; Auto with sets).
+Apply rst_trans with y0; Auto with sets.
 Save.
 
   Lemma clos_rst_is_equiv: (equivalence A (clos_refl_sym_trans A R)).
@@ -83,9 +83,9 @@ Save.
        (incl (clos_refl_sym_trans A (clos_refl_sym_trans A R))
                      (clos_refl_sym_trans A R)).
 Red.
-(Induction 1; Auto with sets).
+Induction 1; Auto with sets.
 Intros.
-(Apply rst_trans with y0; Auto with sets).
+Apply rst_trans with y0; Auto with sets.
 Save.
 
 End Clos_Refl_Sym_Trans.
-- 
cgit v1.2.3