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

1 files changed, 10 insertions, 10 deletions

diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index b03ec80e8..e1fb12f39 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.