aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers')
-rw-r--r--theories/Numbers/Cyclic/Int63/Int63.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index 72c496d56d..febf4fa1be 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -15,6 +15,7 @@ Require Export DoubleType.
Require Import Lia.
Require Import Zpow_facts.
Require Import Zgcd_alt.
+Require ZArith.
Import Znumtheory.
Register bool as kernel.ind_bool.