aboutsummaryrefslogtreecommitdiff
path: root/src/Util/QUtil.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/QUtil.v')
-rw-r--r--src/Util/QUtil.v4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Util/QUtil.v b/src/Util/QUtil.v
index dbdf4fba0..2c2dfd8c8 100644
--- a/src/Util/QUtil.v
+++ b/src/Util/QUtil.v
@@ -1,6 +1,8 @@
Require Import Coq.ZArith.ZArith Coq.QArith.QArith QArith.Qround.
+Require Import Coq.micromega.Lia.
Require Import Crypto.Util.Decidable.
-Require Import ZUtil Lia.
+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Morphisms.
Local Open Scope Z_scope.