diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZDivTrunc.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivTrunc.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index b57f8e27fb..c60bf7c6aa 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -37,13 +37,11 @@ End ZDiv. Module Type ZDivSig := ZAxiomsSig <+ ZDiv. -Module ZDivPropFunct (Import Z : ZDivSig). - (* TODO: en faire un arg du foncteur + comprendre le bug de SearchAbout *) - Module Import ZP := ZPropFunct Z. +Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z). (** We benefit from what already exists for NZ *) - Module Import NZDivP := NZDivPropFunct Z. + Module Import NZDivP := NZDivPropFunct Z ZP. Ltac pos_or_neg a := let LT := fresh "LT" in |