aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/NArith/NArith.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/NArith/NArith.v')
-rw-r--r--theories/NArith/NArith.v5
1 files changed, 0 insertions, 5 deletions
diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v
index 6bfc323d6..4a5f4ee1d 100644
--- a/theories/NArith/NArith.v
+++ b/theories/NArith/NArith.v
@@ -17,11 +17,6 @@ Require Export Nsqrt_def.
Require Export Ngcd_def.
Require Export Ndigits.
Require Export NArithRing.
-Require NBinary.
-
-Module N.
- Include NBinary.N.
-End N.
(** [N] contains an [order] tactic for natural numbers *)