diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZMul.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMul.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v index 4be2ac887..84d840ad2 100644 --- a/theories/Numbers/Integer/Abstract/ZMul.v +++ b/theories/Numbers/Integer/Abstract/ZMul.v @@ -12,9 +12,8 @@ Require Export ZAdd. -Module ZMulPropFunct (Import Z : ZAxiomsSig). +Module ZMulPropFunct (Import Z : ZAxiomsSig'). Include ZAddPropFunct Z. -Local Open Scope NumScope. (** A note on naming: right (correspondingly, left) distributivity happens when the sum is multiplied by a number on the right |