From 9ed53a06a626b82920db6e058835cf2d413ecd56 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 6 Nov 2009 16:43:48 +0000 Subject: 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 --- theories/Numbers/Integer/Abstract/ZAddOrder.v | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'theories/Numbers/Integer/Abstract/ZAddOrder.v') 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. -- cgit v1.2.3