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

7 files changed, 49 insertions, 49 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 1926032733..ca9bea5094 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -19,20 +19,20 @@
 
 Definition RelationalChoice :=
   forall (A B:Type) (R:A -> B -> Prop),
-    (forall x:A,  exists y : B | R x y) ->
-     exists R' : A -> B -> Prop
-    | (forall x:A,
-          exists y : B | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+    (forall x:A,  exists y : B, R x y) ->
+     exists R' : A -> B -> Prop,
+      (forall x:A,
+          exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
 
 Definition FunctionalChoice :=
   forall (A B:Type) (R:A -> B -> Prop),
-    (forall x:A,  exists y : B | R x y) ->
-     exists f : A -> B | (forall x:A, R x (f x)).
+    (forall x:A,  exists y : B, R x y) ->
+     exists f : A -> B, (forall x:A, R x (f x)).
 
 Definition ParamDefiniteDescription :=
   forall (A B:Type) (R:A -> B -> Prop),
-    (forall x:A,  exists y : B | R x y /\ (forall y':B, R x y' -> y = y')) ->
-     exists f : A -> B | (forall x:A, R x (f x)).
+    (forall x:A,  exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) ->
+     exists f : A -> B, (forall x:A, R x (f x)).
 
 Lemma description_rel_choice_imp_funct_choice :
  ParamDefiniteDescription -> RelationalChoice -> FunctionalChoice.
@@ -86,11 +86,11 @@ Qed.
 
 Definition GuardedRelationalChoice :=
   forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop),
-    (forall x:A, P x ->  exists y : B | R x y) ->
-     exists R' : A -> B -> Prop
-    | (forall x:A,
+    (forall x:A, P x ->  exists y : B, R x y) ->
+     exists R' : A -> B -> Prop,
+      (forall x:A,
          P x ->
-          exists y : B | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+          exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
 
 Definition ProofIrrelevance := forall (A:Prop) (a1 a2:A), a1 = a2.
 
@@ -103,7 +103,7 @@ destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as [R' H0].
 intros [x HPx].
 destruct (H x HPx) as [y HRxy].
 exists y; exact HRxy.
-pose (R'' := fun (x:A) (y:B) =>  exists H : P x | R' (existT P x H) y).
+pose (R'' := fun (x:A) (y:B) =>  exists H : P x, R' (existT P x H) y).
 exists R''; intros x HPx.
 destruct (H0 (existT P x HPx)) as [y [HRxy [HR'xy Huniq]]].
 exists y. split.
@@ -120,7 +120,7 @@ Qed.
 
 Definition IndependenceOfPremises :=
   forall (A:Type) (P:A -> Prop) (Q:Prop),
-    (Q ->  exists x : _ | P x) ->  exists x : _ | Q -> P x.
+    (Q ->  exists x : _, P x) ->  exists x : _, Q -> P x.
 
 Lemma rel_choice_indep_of_premises_imp_guarded_rel_choice :
  RelationalChoice -> IndependenceOfPremises -> GuardedRelationalChoice.
@@ -136,4 +136,4 @@ destruct (RelCh A B (fun x y => P x -> R x y)) as [R' H0].
     exists y. split. 
       apply (H1 HPx).
       exact H2.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index 80bbce461c..7b6fcdf53d 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -23,8 +23,8 @@ Require Import ChoiceFacts.
 
 Theorem choice :
  forall (A B:Type) (R:A -> B -> Prop),
-   (forall x:A,  exists y : B | R x y) ->
-    exists f : A -> B | (forall x:A, R x (f x)).
+   (forall x:A,  exists y : B, R x y) ->
+    exists f : A -> B, (forall x:A, R x (f x)).
 Proof.
 apply description_rel_choice_imp_funct_choice.
 exact description.
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 26e696a7cd..a20036f0a5 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -26,15 +26,15 @@ Axiom
   dependent_description :
     forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
       (forall x:A,
-          exists y : B x | R x y /\ (forall y':B x, R x y' -> y = y')) ->
-       exists f : forall x:A, B x | (forall x:A, R x (f x)).
+          exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) ->
+       exists f : forall x:A, B x, (forall x:A, R x (f x)).
 
 (** Principle of definite description (aka axiom of unique choice) *)
 
 Theorem description :
  forall (A B:Type) (R:A -> B -> Prop),
-   (forall x:A,  exists y : B | R x y /\ (forall y':B, R x y' -> y = y')) ->
-    exists f : A -> B | (forall x:A, R x (f x)).
+   (forall x:A,  exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) ->
+    exists f : A -> B, (forall x:A, R x (f x)).
 Proof.
 intros A B.
 apply (dependent_description A (fun _ => B)).
@@ -46,7 +46,7 @@ Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False.
 Proof.
 intro HnotEM.
 pose (R := fun A b => A /\ true = b \/ ~ A /\ false = b).
-assert (H :  exists f : Prop -> bool | (forall A:Prop, R A (f A))).
+assert (H :  exists f : Prop -> bool, (forall A:Prop, R A (f A))).
 apply description.
 intro A.
 destruct (classic A) as [Ha| Hnota].
diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v
index e308eff143..a06be5ae2a 100755
--- a/theories/Logic/Classical_Pred_Set.v
+++ b/theories/Logic/Classical_Pred_Set.v
@@ -18,7 +18,7 @@ Variable U : Set.
 (** de Morgan laws for quantifiers *)
 
 Lemma not_all_ex_not :
- forall P:U -> Prop, ~ (forall n:U, P n) ->  exists n : U | ~ P n.
+ forall P:U -> Prop, ~ (forall n:U, P n) ->  exists n : U, ~ P n.
 Proof.
 unfold not in |- *; intros P notall.
 apply NNPP; unfold not in |- *.
@@ -30,7 +30,7 @@ apply abs; exists n; trivial.
 Qed.
 
 Lemma not_all_not_ex :
- forall P:U -> Prop, ~ (forall n:U, ~ P n) ->  exists n : U | P n.
+ forall P:U -> Prop, ~ (forall n:U, ~ P n) ->  exists n : U, P n.
 Proof.
 intros P H.
 elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n.
@@ -38,7 +38,7 @@ apply NNPP; trivial.
 Qed.
 
 Lemma not_ex_all_not :
- forall P:U -> Prop, ~ ( exists n : U | P n) -> forall n:U, ~ P n.
+ forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n.
 Proof.
 unfold not in |- *; intros P notex n abs.
 apply notex.
@@ -46,7 +46,7 @@ exists n; trivial.
 Qed. 
 
 Lemma not_ex_not_all :
- forall P:U -> Prop, ~ ( exists n : U | ~ P n) -> forall n:U, P n.
+ forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n.
 Proof.
 intros P H n.
 apply NNPP.
@@ -54,14 +54,14 @@ red in |- *; intro K; apply H; exists n; trivial.
 Qed.
 
 Lemma ex_not_not_all :
- forall P:U -> Prop, ( exists n : U | ~ P n) -> ~ (forall n:U, P n).
+ forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n).
 Proof.
 unfold not in |- *; intros P exnot allP.
 elim exnot; auto.
 Qed.
 
 Lemma all_not_not_ex :
- forall P:U -> Prop, (forall n:U, ~ P n) -> ~ ( exists n : U | P n).
+ forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n).
 Proof.
 unfold not in |- *; intros P allnot exP; elim exP; intros n p.
 apply allnot with n; auto.
diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v
index 6bfd08e43e..f3f29747cf 100755
--- a/theories/Logic/Classical_Pred_Type.v
+++ b/theories/Logic/Classical_Pred_Type.v
@@ -18,7 +18,7 @@ Variable U : Type.
 (** de Morgan laws for quantifiers *)
 
 Lemma not_all_ex_not :
- forall P:U -> Prop, ~ (forall n:U, P n) ->  exists n : U | ~ P n.
+ forall P:U -> Prop, ~ (forall n:U, P n) ->  exists n : U, ~ P n.
 Proof.
 unfold not in |- *; intros P notall.
 apply NNPP; unfold not in |- *.
@@ -30,7 +30,7 @@ apply abs; exists n; trivial.
 Qed.
 
 Lemma not_all_not_ex :
- forall P:U -> Prop, ~ (forall n:U, ~ P n) ->  exists n : U | P n.
+ forall P:U -> Prop, ~ (forall n:U, ~ P n) ->  exists n : U, P n.
 Proof.
 intros P H.
 elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n.
@@ -38,7 +38,7 @@ apply NNPP; trivial.
 Qed.
 
 Lemma not_ex_all_not :
- forall P:U -> Prop, ~ ( exists n : U | P n) -> forall n:U, ~ P n.
+ forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n.
 Proof.
 unfold not in |- *; intros P notex n abs.
 apply notex.
@@ -46,7 +46,7 @@ exists n; trivial.
 Qed. 
 
 Lemma not_ex_not_all :
- forall P:U -> Prop, ~ ( exists n : U | ~ P n) -> forall n:U, P n.
+ forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n.
 Proof.
 intros P H n.
 apply NNPP.
@@ -54,14 +54,14 @@ red in |- *; intro K; apply H; exists n; trivial.
 Qed.
 
 Lemma ex_not_not_all :
- forall P:U -> Prop, ( exists n : U | ~ P n) -> ~ (forall n:U, P n).
+ forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n).
 Proof.
 unfold not in |- *; intros P exnot allP.
 elim exnot; auto.
 Qed.
 
 Lemma all_not_not_ex :
- forall P:U -> Prop, (forall n:U, ~ P n) -> ~ ( exists n : U | P n).
+ forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n).
 Proof.
 unfold not in |- *; intros P allnot exP; elim exP; intros n p.
 apply allnot with n; auto.
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index b03ec80e8c..e1fb12f398 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -63,11 +63,11 @@ Variable rel_choice : RelationalChoice.
 
 Lemma guarded_rel_choice :
  forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop),
-   (forall x:A, P x ->  exists y : B | R x y) ->
-    exists R' : A -> B -> Prop
-   | (forall x:A,
+   (forall x:A, P x ->  exists y : B, R x y) ->
+    exists R' : A -> B -> Prop,
+     (forall x:A,
         P x ->
-         exists y : B | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+         exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
 Proof.
   exact
    (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
@@ -79,13 +79,13 @@ Qed.
 Require Import Bool.
 
 Lemma AC :
-  exists R : (bool -> Prop) -> bool -> Prop
- | (forall P:bool -> Prop,
-      ( exists b : bool | P b) ->
-       exists b : bool | P b /\ R P b /\ (forall b':bool, R P b' -> b = b')).
+  exists R : (bool -> Prop) -> bool -> Prop,
+   (forall P:bool -> Prop,
+      (exists b : bool, P b) ->
+       exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b')).
 Proof.
   apply guarded_rel_choice with
-   (P := fun Q:bool -> Prop =>  exists y : _ | Q y)
+   (P := fun Q:bool -> Prop =>  exists y : _, Q y)
    (R := fun (Q:bool -> Prop) (y:bool) => Q y).
   exact (fun _ H => H).
 Qed.
@@ -135,4 +135,4 @@ left; assumption.
 
 Qed.
 
-End PredExt_GuardRelChoice_imp_EM.
\ No newline at end of file
+End PredExt_GuardRelChoice_imp_EM.
diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v
index c55095e473..12c3f746a0 100644
--- a/theories/Logic/RelationalChoice.v
+++ b/theories/Logic/RelationalChoice.v
@@ -13,8 +13,8 @@
 Axiom
   relational_choice :
     forall (A B:Type) (R:A -> B -> Prop),
-      (forall x:A,  exists y : B | R x y) ->
-       exists R' : A -> B -> Prop
-      | (forall x:A,
-            exists y : B
-           | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
\ No newline at end of file
+      (forall x:A,  exists y : B, R x y) ->
+       exists R' : A -> B -> Prop,
+        (forall x:A,
+            exists y : B,
+             R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).