aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/ZUtil.v')
-rw-r--r--src/Util/ZUtil.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 2cfab2e90..db3d84b2d 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1,5 +1,5 @@
-Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv.
-Require Import Omega NPeano Arith.
+Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv.
+Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
Require Import Crypto.Util.NatUtil.
Local Open Scope Z.