diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZDiv.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZDiv.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 5b81cadd2d..db64a79637 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -38,9 +38,8 @@ End NZDiv. Module Type NZDivSig := NZOrdAxiomsSig <+ NZDiv. -Module NZDivPropFunct (Import NZ : NZDivSig). - (* TODO: a transformer un jour en arg funct puis include *) - Module Import P := NZMulOrderPropFunct NZ. +Module NZDivPropFunct + (Import NZ : NZDivSig)(Import NZP : NZMulOrderPropSig NZ). (** Uniqueness theorems *) |