aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Natural/BigN/Nbasic.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Natural/BigN/Nbasic.v')
-rw-r--r--theories/Numbers/Natural/BigN/Nbasic.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index ea472c860d..ed7a7871f4 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -15,8 +15,8 @@ Require Import BigNumPrelude.
Require Import Max.
Require Import DoubleType.
Require Import DoubleBase.
-Require Import Z_nZ.
-Require Import Z_2nZ.
+Require Import CyclicAxioms.
+Require Import DoubleCyclic.
(* To compute the necessary height *)