aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xtheories/Arith/Arith.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index 80c29c3951..b00d155bab 100755
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -16,6 +16,8 @@ Require Export Minus.
Require Export Mult.
Require Export Between.
Require Export Minus.
+Require Export Peano_dec.
+Require Export Compare_dec.
Axiom My_special_variable : nat -> nat.