diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZDivEucl.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index ad8e24cfb1..a853395a68 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -33,9 +33,7 @@ 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 *) @@ -48,7 +46,7 @@ Module ZDivPropFunct (Import Z : ZDivSig). apply le_trans with 0; [ rewrite opp_nonpos_nonneg |]; order. Qed. End Z'. - Module Import NZDivP := NZDivPropFunct Z'. + Module Import NZDivP := NZDivPropFunct Z' ZP. (** Another formulation of the main equation *) |