diff options
Diffstat (limited to 'theories/NArith/NArith.v')
| -rw-r--r-- | theories/NArith/NArith.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index 3a87880ac..0d936ae83 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -15,9 +15,11 @@ Require Export BinNat. Require Export Nnat. Require Export Ndigits. Require Export NArithRing. -Require NBinary Nminmax. +Require NBinary. -Module N := NBinary.N <+ Nminmax.Nextend. +Module N. + Include NBinary.N. +End N. (** [N] contains An [order] tactic for natural numbers *) |