diff options
Diffstat (limited to 'theories/ZArith/Zdiv.v')
| -rw-r--r-- | theories/ZArith/Zdiv.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 06aa2b660..a07b6d038 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -319,7 +319,7 @@ Module ZDivMod := ZBinary.ZBinAxiomsMod <+ ZDiv. (** We hence benefit from generic results about this abstract division. *) -Module Z := ZDivFloor.ZDivPropFunct ZDivMod. +Module Z := ZDivFloor.ZDivPropFunct ZDivMod ZBinary.ZBinPropMod. (** Existence theorem *) |