aboutsummaryrefslogtreecommitdiff
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 b076de2aff..2d54f0e8d9 100644
--- a/theories/Arith/Arith_base.v
+++ b/theories/Arith/Arith_base.v
@@ -18,3 +18,5 @@ Require Export Between.
Require Export Peano_dec.
Require Export Compare_dec.
Require Export Factorial.
+Require Export EqNat.
+Require Export Wf_nat.