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

4 files changed, 7 insertions, 7 deletions

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 665f96c68..e79b5d7c3 100755
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -122,7 +122,7 @@ induction 1; auto with arith.
 Qed.
 
 Lemma exists_in_int :
- forall k l, exists_between k l ->  exists2 m : nat | in_int k l m & Q m.
+ forall k l, exists_between k l ->  exists2 m : nat, in_int k l m & Q m.
 Proof.
 induction 1.
 case IHexists_between; intros p inp Qp; exists p; auto with arith.
@@ -174,7 +174,7 @@ induction 1; intros; auto with arith.
 apply le_trans with (S k); auto with arith.
 Qed.
 
-Definition eventually (n:nat) :=  exists2 k : nat | k <= n & Q k.
+Definition eventually (n:nat) :=  exists2 k : nat, k <= n & Q k.
 
 Lemma event_O : eventually 0 -> Q 0.
 Proof.
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index b5afebd94..b3a85ba06 100755
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -41,7 +41,7 @@ Proof le_lt_or_eq.
 
 (* By special request of G. Kahn - Used in Group Theory *)
 Lemma discrete_nat :
- forall n m, n < m -> S n = m \/ ( exists r : nat | m = S (S (n + r))).
+ forall n m, n < m -> S n = m \/ (exists r : nat, m = S (S (n + r))).
 Proof.
 intros m n H.
 lapply (lt_le_S m n); auto with arith.
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index 02c48f028..b246de635 100644
--- a/theories/Arith/Euclid.v
+++ b/theories/Arith/Euclid.v
@@ -36,7 +36,7 @@ Qed.
 Lemma quotient :
  forall n,
    n > 0 ->
-   forall m:nat, {q : nat |  exists r : nat | m = q * n + r /\ n > r}.
+   forall m:nat, {q : nat |  exists r : nat, m = q * n + r /\ n > r}.
 intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0.
 elim (le_gt_dec b n).
 intro lebn.
@@ -53,7 +53,7 @@ Qed.
 Lemma modulo :
  forall n,
    n > 0 ->
-   forall m:nat, {r : nat |  exists q : nat | m = q * n + r /\ n > r}.
+   forall m:nat, {r : nat |  exists q : nat, m = q * n + r /\ n > r}.
 intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0.
 elim (le_gt_dec b n).
 intro lebn.
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index a7a50795e..6e95af673 100755
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -179,10 +179,10 @@ Variable R : A -> A -> Prop.
 (* Relational form of inversion *)
 Variable F : A -> nat -> Prop.
 Definition inv_lt_rel x y :=
-   exists2 n : _ | F x n & (forall m, F y m -> n < m).
+   exists2 n : _, F x n & (forall m, F y m -> n < m).
 
 Hypothesis F_compat : forall x y:A, R x y -> inv_lt_rel x y.
-Remark acc_lt_rel : forall x:A, ( exists n : _ | F x n) -> Acc R x.
+Remark acc_lt_rel : forall x:A, (exists n : _, F x n) -> Acc R x.
 intros x [n fxn]; generalize x fxn; clear x fxn.
 pattern n in |- *; apply lt_wf_ind; intros.
 constructor; intros.