aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v')
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index db3b622b0..eea29e7ca 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -25,7 +25,7 @@ Require Import DoubleDivn1.
Require Import DoubleDiv.
Require Import CyclicAxioms.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
Section Z_2nZ.