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/NatInt/NZBase.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/NatInt/NZBase.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 7ad38577f..0c9d006d6 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -56,10 +56,7 @@ Section CentralInduction. Variable A : predicate NZ. -Hypothesis A_wd : predicate_wd NZeq A. - -Add Morphism A with signature NZeq ==> iff as A_morph. -Proof. apply A_wd. Qed. +Hypothesis A_wd : Proper (NZeq==>iff) A. Theorem NZcentral_induction : forall z : NZ, A z -> |