diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-03 08:24:34 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-03 08:24:34 +0000 |
| commit | 288c8de205667afc00b340556b0b8c98ffa77459 (patch) | |
| tree | 40c77b6c241ed39ce64e59ead13b35bd57d7c299 /theories/Numbers/Integer/Abstract | |
| parent | 4ade23ef522409d0754198ea35747a65b6fa9d81 (diff) | |
Numbers: start using Classes stuff, Equivalence, Proper, Instance, etc
TODO: finish removing the "Add Relation", "Add Morphism" fun_* fun2_*
TODO: now that we have Include, flatten the hierarchy...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12464 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer/Abstract')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZBase.v | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index dfffe9a7f..bd6db10d9 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -48,7 +48,7 @@ Parameter Zopp : Z -> Z. (*Notation "- 1" := (Zopp 1) : IntScope. Check (-1).*) -Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd. +Instance Zopp_wd : Proper (Zeq==>Zeq) Zopp. Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope. Notation "- 1" := (Zopp (NZsucc NZ0)) : IntScope. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 648cde197..7b3c0ba6e 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -34,13 +34,13 @@ Theorem Zpred_succ : forall n : Z, P (S n) == n. Proof NZpred_succ. Theorem Zeq_refl : forall n : Z, n == n. -Proof (proj1 NZeq_equiv). +Proof (@Equivalence_Reflexive _ _ NZeq_equiv). Theorem Zeq_sym : forall n m : Z, n == m -> m == n. -Proof (proj2 (proj2 NZeq_equiv)). +Proof (@Equivalence_Symmetric _ _ NZeq_equiv). Theorem Zeq_trans : forall n m p : Z, n == m -> m == p -> n == p. -Proof (proj1 (proj2 NZeq_equiv)). +Proof (@Equivalence_Transitive _ _ NZeq_equiv). Theorem Zneq_sym : forall n m : Z, n ~= m -> m ~= n. Proof NZneq_sym. |