diff options
Diffstat (limited to 'theories/Numbers/Natural/Axioms/NTimes.v')
| -rw-r--r-- | theories/Numbers/Natural/Axioms/NTimes.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Axioms/NTimes.v index 6a7e9ba39e..4d1d2b0cad 100644 --- a/theories/Numbers/Natural/Axioms/NTimes.v +++ b/theories/Numbers/Natural/Axioms/NTimes.v @@ -15,7 +15,7 @@ Axiom times_Sn_m : forall n m, (S n) * m == m + n * m. End TimesSignature. -Module TimesProperties (Import TimesModule : TimesSignature). +Module TimesProperties (Export TimesModule : TimesSignature). Module Export PlusPropertiesModule := PlusProperties PlusModule. Open Local Scope NScope. |