diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZDivFloor.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivFloor.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index fd052c2ef..c619d8b07 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -34,10 +34,10 @@ End ZDivSpecific. Module Type ZDiv (Z:ZAxiomsSig) := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. -Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv. -Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation. +Module Type ZDivSig := ZAxiomsSig <+ ZDiv. +Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation. -Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). +Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z). (** We benefit from what already exists for NZ *) @@ -50,7 +50,7 @@ Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. Proof. intros. now apply mod_pos_bound. Qed. End ZD. - Module Import NZDivP := NZDivPropFunct Z ZP ZD. + Module Import NZDivP := NZDivProp Z ZP ZD. (** Another formulation of the main equation *) @@ -628,5 +628,5 @@ rewrite Hc, mul_comm. now apply mod_mul. Qed. -End ZDivPropFunct. +End ZDivProp. |