modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes

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

11 files changed, 37 insertions, 37 deletions

diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index 0d77c0617..59f8fb2c8 100755
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -67,7 +67,7 @@ Inductive Totally_ordered (B:Ensemble U) : Prop :=
 Definition Compatible : Relation U :=
   fun x y:U =>
     In U C x ->
-    In U C y ->  exists z : _ | In U C z /\ Upper_Bound (Couple U x y) z.
+    In U C y ->  exists z : _, In U C z /\ Upper_Bound (Couple U x y) z.
 	
 Inductive Directed (X:Ensemble U) : Prop :=
     Definition_of_Directed :
@@ -75,21 +75,21 @@ Inductive Directed (X:Ensemble U) : Prop :=
       Inhabited U X ->
       (forall x1 x2:U,
          Included U (Couple U x1 x2) X ->
-          exists x3 : _ | In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) ->
+          exists x3 : _, In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) ->
       Directed X.
 
 Inductive Complete : Prop :=
     Definition_of_Complete :
-      ( exists bot : _ | Bottom bot) ->
-      (forall X:Ensemble U, Directed X ->  exists bsup : _ | Lub X bsup) ->
+      (exists bot : _, Bottom bot) ->
+      (forall X:Ensemble U, Directed X ->  exists bsup : _, Lub X bsup) ->
       Complete.
 
 Inductive Conditionally_complete : Prop :=
     Definition_of_Conditionally_complete :
       (forall X:Ensemble U,
          Included U X C ->
-         ( exists maj : _ | Upper_Bound X maj) ->
-          exists bsup : _ | Lub X bsup) -> Conditionally_complete.
+         (exists maj : _, Upper_Bound X maj) ->
+          exists bsup : _, Lub X bsup) -> Conditionally_complete.
 End Bounds.
 Hint Resolve Totally_ordered_definition Upper_Bound_definition
   Lower_Bound_definition Lub_definition Glb_definition Bottom_definition
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index 28b2d6fb9..dce4c64e8 100755
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -59,8 +59,8 @@ Lemma cardinal_invert :
    match p with
    | O => X = Empty_set U
    | S n =>
-        exists A : _
-       | ( exists x : _ | X = Add U A x /\ ~ In U A x /\ cardinal U A n)
+        exists A : _,
+         (exists x : _, X = Add U A x /\ ~ In U A x /\ cardinal U A n)
    end.
 Proof.
 induction 1; simpl in |- *; auto.
@@ -78,4 +78,4 @@ Proof.
 intros X p C; elim C; simpl in |- *; trivial with sets.
 Qed.
 
-End Ensembles_finis_facts.
\ No newline at end of file
+End Ensembles_finis_facts.
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index 2849bce6c..f394b2e5a 100755
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -40,7 +40,7 @@ Section Finite_sets_facts.
 Variable U : Type.
 
 Lemma finite_cardinal :
- forall X:Ensemble U, Finite U X ->  exists n : nat | cardinal U X n.
+ forall X:Ensemble U, Finite U X ->  exists n : nat, cardinal U X n.
 Proof.
 induction 1 as [| A _ [n H]].
 exists 0; auto with sets.
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index 85b83d3ab..fd1c90b90 100755
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -93,7 +93,7 @@ Hint Resolve finite_image.
 
 Lemma Im_inv :
  forall (X:Ensemble U) (f:U -> V) (y:V),
-   In _ (Im X f) y ->  exists x : U | In _ X x /\ f x = y.
+   In _ (Im X f) y ->  exists x : U, In _ X x /\ f x = y.
 Proof.
 intros X f y H'; elim H'.
 intros x H'0 y0 H'1; rewrite H'1.
@@ -104,14 +104,14 @@ Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y.
 
 Lemma not_injective_elim :
  forall f:U -> V,
-   ~ injective f ->  exists x : _ | ( exists y : _ | f x = f y /\ x <> y).
+   ~ injective f ->  exists x : _, (exists y : _, f x = f y /\ x <> y).
 Proof.
 unfold injective in |- *; intros f H.
-cut ( exists x : _ | ~ (forall y:U, f x = f y -> x = y)).
+cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)).
 2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y);
     trivial with sets.
 destruct 1 as [x C]; exists x.
-cut ( exists y : _ | ~ (f x = f y -> x = y)).
+cut (exists y : _, ~ (f x = f y -> x = y)).
 2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y);
     trivial with sets.
 destruct 1 as [y D]; exists y.
@@ -120,7 +120,7 @@ Qed.
 
 Lemma cardinal_Im_intro :
  forall (A:Ensemble U) (f:U -> V) (n:nat),
-   cardinal _ A n ->  exists p : nat | cardinal _ (Im A f) p.
+   cardinal _ A n ->  exists p : nat, cardinal _ (Im A f) p.
 Proof.
 intros.
 apply finite_cardinal; apply finite_image.
@@ -196,7 +196,7 @@ Lemma Pigeonhole_principle :
    cardinal _ A n ->
    forall n':nat,
      cardinal _ (Im A f) n' ->
-     n' < n ->  exists x : _ | ( exists y : _ | f x = f y /\ x <> y).
+     n' < n ->  exists x : _, (exists y : _, f x = f y /\ x <> y).
 Proof.
 intros; apply not_injective_elim.
 apply Pigeonhole with A n n'; trivial with sets.
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index 20ec73fa6..d401b86c1 100755
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -67,7 +67,7 @@ Lemma approximants_grow :
    ~ Finite U A ->
    forall n:nat,
      cardinal U X n ->
-     Included U X A ->  exists Y : _ | cardinal U Y (S n) /\ Included U Y A.
+     Included U X A ->  exists Y : _, cardinal U Y (S n) /\ Included U Y A.
 Proof.
 intros A X H' n H'0; elim H'0; auto with sets.
 intro H'1.
@@ -108,12 +108,12 @@ Lemma approximants_grow' :
    forall n:nat,
      cardinal U X n ->
      Approximant U A X ->
-      exists Y : _ | cardinal U Y (S n) /\ Approximant U A Y.
+      exists Y : _, cardinal U Y (S n) /\ Approximant U A Y.
 Proof.
 intros A X H' n H'0 H'1; try assumption.
 elim H'1.
 intros H'2 H'3.
-elimtype ( exists Y : _ | cardinal U Y (S n) /\ Included U Y A).
+elimtype (exists Y : _, cardinal U Y (S n) /\ Included U Y A).
 intros x H'4; elim H'4; intros H'5 H'6; try exact H'5; clear H'4.
 exists x; auto with sets.
 split; [ auto with sets | idtac ].
@@ -125,7 +125,7 @@ Qed.
 Lemma approximant_can_be_any_size :
  forall A X:Ensemble U,
    ~ Finite U A ->
-   forall n:nat,  exists Y : _ | cardinal U Y n /\ Approximant U A Y.
+   forall n:nat,  exists Y : _, cardinal U Y n /\ Approximant U A Y.
 Proof.
 intros A H' H'0 n; elim n.
 exists (Empty_set U); auto with sets.
@@ -140,8 +140,8 @@ Theorem Image_set_continuous :
  forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
    Finite V X ->
    Included V X (Im U V A f) ->
-    exists n : _
-   | ( exists Y : _ | (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X).
+    exists n : _,
+     (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X).
 Proof.
 intros A f X H'; elim H'.
 intro H'0; exists 0.
@@ -183,12 +183,12 @@ Qed.
 Theorem Image_set_continuous' :
  forall (A:Ensemble U) (f:U -> V) (X:Ensemble V),
    Approximant V (Im U V A f) X ->
-    exists Y : _ | Approximant U A Y /\ Im U V Y f = X.
+    exists Y : _, Approximant U A Y /\ Im U V Y f = X.
 Proof.
 intros A f X H'; try assumption.
 cut
- ( exists n : _
-  | ( exists Y : _ | (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)).
+ (exists n : _,
+    (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)).
 intro H'0; elim H'0; intros n E; elim E; clear H'0.
 intros x H'0; try assumption.
 elim H'0; intros H'1 H'2; elim H'1; intros H'3 H'4; try exact H'3;
@@ -241,4 +241,4 @@ red in |- *; intro H'2.
 elim (Pigeonhole_bis A f); auto with sets.
 Qed.
 
-End Infinite_sets.
\ No newline at end of file
+End Infinite_sets.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 7f8e1695a..c9121032d 100755
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -99,7 +99,7 @@ Hint Resolve le_total_order.
 
 Lemma Finite_subset_has_lub :
  forall X:Ensemble nat,
-   Finite nat X ->  exists m : nat | Upper_Bound nat nat_po X m.
+   Finite nat X ->  exists m : nat, Upper_Bound nat nat_po X m.
 Proof.
 intros X H'; elim H'.
 exists 0.
@@ -138,7 +138,7 @@ intros x1 H'1; elim H'1; auto with sets arith.
 Qed.
 
 Lemma Integers_has_no_ub :
- ~ ( exists m : nat | Upper_Bound nat nat_po Integers m).
+ ~ (exists m : nat, Upper_Bound nat nat_po Integers m).
 Proof.
 red in |- *; intro H'; elim H'.
 intros x H'0.
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 5ef6bc9b0..15fc690dd 100755
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -48,7 +48,7 @@ Definition Strict_Rel_of : Rel := fun x y:U => Rel_of p x y /\ x <> y.
 Inductive covers (y x:U) : Prop :=
     Definition_of_covers :
       Strict_Rel_of x y ->
-      ~ ( exists z : _ | Strict_Rel_of x z /\ Strict_Rel_of z y) ->
+      ~ (exists z : _, Strict_Rel_of x z /\ Strict_Rel_of z y) ->
       covers y x.
 
 End Partial_orders.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 988bbd25a..71ec5b078 100755
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -177,7 +177,7 @@ Qed.
 Lemma Included_Add :
  forall (X A:Ensemble U) (x:U),
    Included U X (Add U A x) ->
-   Included U X A \/ ( exists A' : _ | X = Add U A' x /\ Included U A' A).
+   Included U X A \/ (exists A' : _, X = Add U A' x /\ Included U A' A).
 Proof.
 intros X A x H'0; try assumption.
 elim (classic (In U X x)).
@@ -267,7 +267,7 @@ Theorem covers_Add :
    Included U a A ->
    Included U a' A ->
    covers (Ensemble U) (Power_set_PO U A) a' a ->
-    exists x : _ | a' = Add U a x /\ In U A x /\ ~ In U a x.
+    exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x.
 Proof.
 intros A a a' H' H'0 H'1; try assumption.
 elim (setcover_inv A a a'); auto with sets.
@@ -299,7 +299,7 @@ Theorem covers_is_Add :
    Included U a A ->
    Included U a' A ->
    (covers (Ensemble U) (Power_set_PO U A) a' a <->
-    ( exists x : _ | a' = Add U a x /\ In U A x /\ ~ In U a x)).
+    (exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x)).
 Proof.
 intros A a a' H' H'0; split; intro K.
 apply covers_Add with (A := A); auto with sets.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index c587744a3..91018f05e 100755
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -254,7 +254,7 @@ Qed.
 Lemma setcover_intro :
  forall (U:Type) (A x y:Ensemble U),
    Strict_Included U x y ->
-   ~ ( exists z : _ | Strict_Included U x z /\ Strict_Included U z y) ->
+   ~ (exists z : _, Strict_Included U x z /\ Strict_Included U z y) ->
    covers (Ensemble U) (Power_set_PO U A) y x.
 Proof.
 intros; apply Definition_of_covers; auto with sets.
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index 4fda8d8e9..2a0aaf98b 100755
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -67,7 +67,7 @@ Qed.
 
 Theorem Rstar_cases :
  forall (U:Type) (R:Relation U) (x y:U),
-   Rstar U R x y -> x = y \/ ( exists u : _ | R x u /\ Rstar U R u y).
+   Rstar U R x y -> x = y \/ (exists u : _, R x u /\ Rstar U R u y).
 Proof.
 intros U R x y H'; elim H'; auto with sets.
 intros x0 y0 z H'0 H'1 H'2; right; exists y0; auto with sets.
@@ -116,7 +116,7 @@ Qed.
 
 Theorem RstarRplus_RRstar :
  forall (U:Type) (R:Relation U) (x y z:U),
-   Rstar U R x y -> Rplus U R y z ->  exists u : _ | R x u /\ Rstar U R u z.
+   Rstar U R x y -> Rplus U R y z ->  exists u : _, R x u /\ Rstar U R u z.
 Proof.
 generalize Rstar_contains_Rplus; intro T; red in T.
 generalize Rstar_transitive; intro T1; red in T1.
@@ -134,7 +134,7 @@ Theorem Lemma1 :
    Strongly_confluent U R ->
    forall x b:U,
      Rstar U R x b ->
-     forall a:U, R x a ->  exists z : _ | Rstar U R a z /\ R b z.
+     forall a:U, R x a ->  exists z : _, Rstar U R a z /\ R b z.
 Proof.
 intros U R H' x b H'0; elim H'0.
 intros x0 a H'1; exists a; auto with sets.
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index 1fe689002..d84884d41 100755
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -34,7 +34,7 @@ Section Relations_3.
    Variable R : Relation U.
    
    Definition coherent (x y:U) : Prop :=
-      exists z : _ | Rstar U R x z /\ Rstar U R y z.
+      exists z : _, Rstar U R x z /\ Rstar U R y z.
    
    Definition locally_confluent (x:U) : Prop :=
      forall y z:U, R x y -> R x z -> coherent y z.