Parentheses

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

4 files changed, 31 insertions, 31 deletions

diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index 0db6c1012..9b2f57809 100755
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -146,8 +146,8 @@ Theorem Union_is_Lub:
 Intros A a b H' H'0.
 Apply Lub_definition; Simpl.
 Apply Upper_Bound_definition; Simpl; Auto with sets.
-(Intros y H'1; Elim H'1); Auto with sets.
-(Intros y H'1; Elim H'1); Simpl; Auto with sets.
+Intros y H'1; Elim H'1; Auto with sets.
+Intros y H'1; Elim H'1; Simpl; Auto with sets.
 Qed.
 
 Theorem Intersection_is_Glb:
@@ -162,8 +162,8 @@ Apply Glb_definition; Simpl.
 Apply Lower_Bound_definition; Simpl; Auto with sets.
 Apply Definition_of_Power_set.
 Generalize Inclusion_is_transitive; Intro IT; Red in IT; Apply IT with a; Auto with sets.
-(Intros y H'1; Elim H'1); Auto with sets.
-(Intros y H'1; Elim H'1); Simpl; Auto with sets.
+Intros y H'1; Elim H'1; Auto with sets.
+Intros y H'1; Elim H'1; Simpl; Auto with sets.
 Qed.
 
 End The_power_set_partial_order.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index b886f1211..57e51123d 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_2_facts.v b/theories/Sets/Relations_2_facts.v
index d5854165a..05f3753be 100755
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -38,7 +38,7 @@ Qed.
 Theorem Rstar_contains_R :
   (U: Type) (R: (Relation U)) (contains U (Rstar U R) R).
 Proof.
-(Intros U R; Red); Intros x y H'; Apply Rstar_n with y; Auto with sets.
+Intros U R; Red; Intros x y H'; Apply Rstar_n with y; Auto with sets.
 Qed.
 
 Theorem Rstar_contains_Rplus :
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index 6b1e763de..f7278ba2a 100755
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -47,20 +47,20 @@ Theorem Strong_confluence :
   (U: Type) (R: (Relation U)) (Strongly_confluent U R) -> (Confluent U R).
 Proof.
 Intros U R H'; Red.
-(Intro x; Red); Intros a b H'0.
+Intro x; Red; Intros a b H'0.
 Unfold 1 coherent.
 Generalize b; Clear b.
 Elim H'0; Clear H'0.
 Intros x0 b H'1; Exists b; Auto with sets.
 Intros x0 y z H'1 H'2 H'3 b H'4.
-(Generalize (Lemma1 U R); Intro h; LApply h;
+Generalize (Lemma1 U R); Intro h; LApply h;
   [Intro H'0; Generalize (H'0 x0 b); Intro h0; LApply h0;
     [Intro H'5; Generalize (H'5 y); Intro h1; LApply h1;
       [Intro h2; Elim h2; Intros z0 h3; Elim h3; Intros H'6 H'7;
-        Clear h h0 h1 h2 h3 | Clear h h0 h1] | Clear h h0] | Clear h]); Auto with sets.
-(Generalize (H'3 z0); Intro h; LApply h;
+        Clear h h0 h1 h2 h3 | Clear h h0 h1] | Clear h h0] | Clear h]; Auto with sets.
+Generalize (H'3 z0); Intro h; LApply h;
   [Intro h0; Elim h0; Intros z1 h1; Elim h1; Intros H'8 H'9; Clear h h0 h1 |
-    Clear h]); Auto with sets.
+    Clear h]; Auto with sets.
 Exists z1; Split; Auto with sets.
 Apply Rstar_n with z0; Auto with sets.
 Qed.
@@ -69,7 +69,7 @@ Theorem Strong_confluence_direct :
   (U: Type) (R: (Relation U)) (Strongly_confluent U R) -> (Confluent U R).
 Proof.
 Intros U R H'; Red.
-(Intro x; Red); Intros a b H'0.
+Intro x; Red; Intros a b H'0.
 Unfold 1 coherent.
 Generalize b; Clear b.
 Elim H'0; Clear H'0.
@@ -77,9 +77,9 @@ Intros x0 b H'1; Exists b; Auto with sets.
 Intros x0 y z H'1 H'2 H'3 b H'4.
 Cut (exT U [t: U] (Rstar U R y t) /\ (R b t)).
 Intro h; Elim h; Intros t h0; Elim h0; Intros H'0 H'5; Clear h h0.
-(Generalize (H'3 t); Intro h; LApply h;
+Generalize (H'3 t); Intro h; LApply h;
   [Intro h0; Elim h0; Intros z0 h1; Elim h1; Intros H'6 H'7; Clear h h0 h1 |
-    Clear h]); Auto with sets.
+    Clear h]; Auto with sets.
 Exists z0; Split; [Assumption | Idtac].
 Apply Rstar_n with t; Auto with sets.
 Generalize H'1; Generalize y; Clear H'1.
@@ -87,13 +87,13 @@ Elim H'4.
 Intros x1 y0 H'0; Exists y0; Auto with sets.
 Intros x1 y0 z0 H'0 H'1 H'5 y1 H'6.
 Red in H'.
-(Generalize (H' x1 y0 y1); Intro h; LApply h;
+Generalize (H' x1 y0 y1); Intro h; LApply h;
   [Intro H'7; LApply H'7;
     [Intro h0; Elim h0; Intros z1 h1; Elim h1; Intros H'8 H'9; Clear h H'7 h0 h1 |
-      Clear h] | Clear h]); Auto with sets.
-(Generalize (H'5 z1); Intro h; LApply h;
+      Clear h] | Clear h]; Auto with sets.
+Generalize (H'5 z1); Intro h; LApply h;
   [Intro h0; Elim h0; Intros t h1; Elim h1; Intros H'7 H'10; Clear h h0 h1 |
-    Clear h]); Auto with sets.
+    Clear h]; Auto with sets.
 Exists t; Split; Auto with sets.
 Apply Rstar_n with z1; Auto with sets.
 Qed.
@@ -111,40 +111,40 @@ Theorem Newman :
   (U: Type) (R: (Relation U)) (Noetherian U R) -> (Locally_confluent U R) ->
    (Confluent U R).
 Proof.
-(Intros U R H' H'0; Red); Intro x.
+Intros U R H' H'0; Red; Intro x.
 Elim (H' x); Unfold confluent.
 Intros x0 H'1 H'2 y z H'3 H'4.
-(Generalize (Rstar_cases U R x0 y); Intro h; LApply h;
+Generalize (Rstar_cases U R x0 y); Intro h; LApply h;
   [Intro h0; Elim h0;
     [Clear h h0; Intro h1 |
       Intro h1; Elim h1; Intros u h2; Elim h2; Intros H'5 H'6; Clear h h0 h1 h2] |
-    Clear h]); Auto with sets.
+    Clear h]; Auto with sets.
 Elim h1; Auto with sets.
-(Generalize (Rstar_cases U R x0 z); Intro h; LApply h;
+Generalize (Rstar_cases U R x0 z); Intro h; LApply h;
   [Intro h0; Elim h0;
     [Clear h h0; Intro h1 |
       Intro h1; Elim h1; Intros v h2; Elim h2; Intros H'7 H'8; Clear h h0 h1 h2] |
-    Clear h]); Auto with sets.
+    Clear h]; Auto with sets.
 Elim h1; Generalize coherent_symmetric; Intro t; Red in t; Auto with sets.
 Unfold Locally_confluent locally_confluent coherent in H'0.
-(Generalize (H'0 x0 u v); Intro h; LApply h;
+Generalize (H'0 x0 u v); Intro h; LApply h;
   [Intro H'9; LApply H'9;
     [Intro h0; Elim h0; Intros t h1; Elim h1; Intros H'10 H'11;
-      Clear h H'9 h0 h1 | Clear h] | Clear h]); Auto with sets.
+      Clear h H'9 h0 h1 | Clear h] | Clear h]; Auto with sets.
 Clear H'0.
 Unfold 1 coherent in H'2.
-(Generalize (H'2 u); Intro h; LApply h;
+Generalize (H'2 u); Intro h; LApply h;
   [Intro H'0; Generalize (H'0 y t); Intro h0; LApply h0;
     [Intro H'9; LApply H'9;
       [Intro h1; Elim h1; Intros y1 h2; Elim h2; Intros H'12 H'13;
-        Clear h h0 H'9 h1 h2 | Clear h h0] | Clear h h0] | Clear h]); Auto with sets.
+        Clear h h0 H'9 h1 h2 | Clear h h0] | Clear h h0] | Clear h]; Auto with sets.
 Generalize Rstar_transitive; Intro T; Red in T.
-(Generalize (H'2 v); Intro h; LApply h;
+Generalize (H'2 v); Intro h; LApply h;
   [Intro H'9; Generalize (H'9 y1 z); Intro h0; LApply h0;
     [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.
+        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.
 Apply T with y1; Auto with sets.
 Apply T with t; Auto with sets.
 Qed.