diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-06 16:43:48 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-06 16:43:48 +0000 |
| commit | 9ed53a06a626b82920db6e058835cf2d413ecd56 (patch) | |
| tree | 6bd4efe0d8679f9a3254091e6f1d64b1b2462ec2 /theories/Numbers/Integer/Abstract/ZAddOrder.v | |
| parent | 625a129d5e9b200399a147111f191abe84282aa4 (diff) | |
Numbers: more (syntactic) changes toward new style of type classes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12475 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZAddOrder.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAddOrder.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index 917e3fc12..5f68b2bb1 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -350,9 +350,7 @@ Qed. Section PosNeg. Variable P : Z -> Prop. -Hypothesis P_wd : predicate_wd Zeq P. - -Add Morphism P with signature Zeq ==> iff as P_morph. Proof. exact P_wd. Qed. +Hypothesis P_wd : Proper (Zeq ==> iff) P. Theorem Z0_pos_neg : P 0 -> (forall n : Z, 0 < n -> P n /\ P (- n)) -> forall n : Z, P n. |