aboutsummaryrefslogtreecommitdiff
path: root/src/BaseSystem.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/BaseSystem.v')
-rw-r--r--src/BaseSystem.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/BaseSystem.v b/src/BaseSystem.v
index 627550440..e6ad55f18 100644
--- a/src/BaseSystem.v
+++ b/src/BaseSystem.v
@@ -1,7 +1,7 @@
-Require Import List.
-Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
-Require Import ZArith.ZArith ZArith.Zdiv.
-Require Import Omega NPeano Arith.
+Require Import Coq.Lists.List.
+Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
+Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
+Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
Local Open Scope Z.