aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/Arith_base.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Arith/Arith_base.v')
-rw-r--r--theories/Arith/Arith_base.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
index 9f0f05db4..290ce548a 100644
--- a/theories/Arith/Arith_base.v
+++ b/theories/Arith/Arith_base.v
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+Require Export PeanoNat.
+
Require Export Le.
Require Export Lt.
Require Export Plus.