aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Cyclic/DoubleCyclic
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Cyclic/DoubleCyclic')
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v (renamed from theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v)2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 26d2393f9..54ff3d354 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/Z_2nZ.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -23,7 +23,7 @@ Require Import DoubleSqrt.
Require Import DoubleLift.
Require Import DoubleDivn1.
Require Import DoubleDiv.
-Require Import Z_nZ.
+Require Import CyclicAxioms.
Open Local Scope Z_scope.