diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-09-28 17:30:26 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-09-28 17:30:32 +0200 |
| commit | 1c3bc5642fe29855cc4d72aa677ff7ffd4787271 (patch) | |
| tree | d574219670e9fbb01a848e87aa6eab6347b1738c /theories/Numbers | |
| parent | 6a5f10f725a1e10a88df404574331c9f679bc474 (diff) | |
ZDivEucl: notations in different scope to avoid a warning
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index 278e1bcff..c2fa69e53 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -30,18 +30,23 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. We just ignore them here. *) -Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod' A). - Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= a mod b < abs b. +Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod A). + Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= B.modulo a b < abs b. End EuclidSpec. Module Type ZEuclid (Z:ZAxiomsSig) := NZDiv.NZDiv Z <+ EuclidSpec Z. -Module Type ZEuclid' (Z:ZAxiomsSig) := NZDiv.NZDiv' Z <+ EuclidSpec Z. Module ZEuclidProp (Import A : ZAxiomsSig') (Import B : ZMulOrderProp A) (Import C : ZSgnAbsProp A B) - (Import D : ZEuclid' A). + (Import D : ZEuclid A). + + (** We put notations in a scope, to avoid warnings about + redefinitions of notations *) + Infix "/" := D.div : euclid. + Infix "mod" := D.modulo : euclid. + Local Open Scope euclid. Module Import Private_NZDiv := Nop <+ NZDivProp A D B. @@ -615,4 +620,3 @@ intros (c,Hc). rewrite Hc. now apply mod_mul. Qed. End ZEuclidProp. - |