aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-10-31 22:02:48 +0100
committerPierre-Marie Pédrot2019-10-31 22:02:48 +0100
commit82461ff590360a1223fad69446b77f535d28b6b4 (patch)
tree4d9a369a9a567e0850d6ae006fb029ba8675ebfc /theories/Numbers
parent151b84a3540d1972d53460780396f2749d0378cf (diff)
parentc0fd4618ac7d35de8658fdcf626cdf26c0cca415 (diff)
Merge PR #10983: QArith, Lia: depend on ZArith_base rather than on ZArith
Ack-by: fajb Reviewed-by: ppedrot
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.