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

5 files changed, 5 insertions, 5 deletions

diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 4c2efceb17..1b1cf27d20 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -35,7 +35,7 @@ Open Local Scope Z_scope.
   Then the  diagram will be closed and the theorem proved. *)
 
 Lemma Z_of_nat_complete :
- forall x:Z, 0 <= x ->  exists n : nat | x = Z_of_nat n.
+ forall x:Z, 0 <= x ->  exists n : nat, x = Z_of_nat n.
 intro x; destruct x; intros;
  [ exists 0%nat; auto with arith
  | specialize (ZL4 p); intros Hp; elim Hp; intros; exists (S x); intros;
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index f7015089c5..d11242c853 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -93,7 +93,7 @@ Hint Local Resolve Pcompare_refl.
 (** Comparison first-order specification *)
 
 Lemma Zcompare_Gt_spec :
- forall n m:Z, (n ?= m) = Gt ->  exists h : positive | n + - m = Zpos h.
+ forall n m:Z, (n ?= m) = Gt ->  exists h : positive, n + - m = Zpos h.
 Proof.
 intros x y; case x; case y;
  [ simpl in |- *; intros H; discriminate H
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index ba6d21c4d8..30065d7054 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -236,7 +236,7 @@ Fixpoint Is_power (p:positive) : Prop :=
   end.
 
 Lemma Is_power_correct :
- forall p:positive, Is_power p <-> ( exists y : nat | p = shift_nat y 1).
+ forall p:positive, Is_power p <-> (exists y : nat, p = shift_nat y 1).
 
 split;
  [ elim p;
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index d9bc4d1b2b..a0027efb33 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -97,7 +97,7 @@ intros x y H; rewrite H; trivial with arith.
 Qed.
 
 Theorem intro_Z :
- forall n:nat,  exists y : Z | Z_of_nat n = y /\ 0 <= y * 1 + 0.
+ forall n:nat,  exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
 Proof.
 intros x; exists (Z_of_nat x); split;
  [ trivial with arith
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index f560050804..ede579586c 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -17,7 +17,7 @@ Open Local Scope Z_scope.
 (** Definition and properties of square root on Z *)
 
 (** The following tactic replaces all instances of (POS (xI ...)) by
-    `2*(POS ...)+1` , but only when ... is not made only with xO, XI, or xH. *)
+    `2*(POS ...)+1`, but only when ... is not made only with xO, XI, or xH. *)
 Ltac compute_POS :=
   match goal with
   |  |- context [(Zpos (xI ?X1))] =>