diff options
| author | letouzey | 2010-01-04 17:50:38 +0000 |
|---|---|---|
| committer | letouzey | 2010-01-04 17:50:38 +0000 |
| commit | b63cd131e8b4a5600973c860d2ccc6e3e5c8ce91 (patch) | |
| tree | b544d2675d0e40b9430abe2a923f70de5357fdb5 /theories/Numbers/NatInt | |
| parent | 883bea94e52fff9cee76894761d3704872d7a61d (diff) | |
Specific syntax for Instances in Module Type: Declare Instance
NB: the grammar entry is placed in vernac:command on purpose
even if it should have gone into vernac:gallina_ext. Camlp4
isn't factorising rules starting by "Declare" in a correct way
otherwise...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12623 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/NatInt')
| -rw-r--r-- | theories/Numbers/NatInt/NZAxioms.v | 12 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZDiv.v | 4 |
2 files changed, 8 insertions, 8 deletions
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index ff220e7933..f6328e2498 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -37,8 +37,8 @@ Notation S := succ. Notation P := pred. Notation "1" := (S 0) : NumScope. -Instance succ_wd : Proper (eq ==> eq) S. -Instance pred_wd : Proper (eq ==> eq) P. +Declare Instance succ_wd : Proper (eq ==> eq) S. +Declare Instance pred_wd : Proper (eq ==> eq) P. Axiom pred_succ : forall n, P (S n) == n. @@ -67,9 +67,9 @@ Notation "x + y" := (add x y) : NumScope. Notation "x - y" := (sub x y) : NumScope. Notation "x * y" := (mul x y) : NumScope. -Instance add_wd : Proper (eq ==> eq ==> eq) add. -Instance sub_wd : Proper (eq ==> eq ==> eq) sub. -Instance mul_wd : Proper (eq ==> eq ==> eq) mul. +Declare Instance add_wd : Proper (eq ==> eq ==> eq) add. +Declare Instance sub_wd : Proper (eq ==> eq ==> eq) sub. +Declare Instance mul_wd : Proper (eq ==> eq ==> eq) mul. Axiom add_0_l : forall n, (0 + n) == n. Axiom add_succ_l : forall n m, (S n) + m == S (n + m). @@ -107,7 +107,7 @@ Notation "x <= y <= z" := (x<=y /\ y<=z) : NumScope. Notation "x <= y < z" := (x<=y /\ y<z) : NumScope. Notation "x < y <= z" := (x<y /\ y<=z) : NumScope. -Instance lt_wd : Proper (eq ==> eq ==> iff) lt. +Declare Instance lt_wd : Proper (eq ==> eq ==> iff) lt. (** Compatibility of [le] can be proved later from [lt_wd] and [lt_eq_cases] *) diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 62eee289d3..1be2f85087 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -20,8 +20,8 @@ Module Type NZDiv (Import NZ : NZOrdAxiomsSig). Infix "/" := div : NumScope. Infix "mod" := modulo (at level 40, no associativity) : NumScope. - Instance div_wd : Proper (eq==>eq==>eq) div. - Instance mod_wd : Proper (eq==>eq==>eq) modulo. + Declare Instance div_wd : Proper (eq==>eq==>eq) div. + Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo. Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b). Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. |