aboutsummaryrefslogtreecommitdiff
path: root/src/Galois
diff options
context:
space:
mode:
authorGravatar Rob Sloan <varomodt@gmail.com>2016-01-11 05:26:11 -0500
committerGravatar Rob Sloan <varomodt@gmail.com>2016-01-11 05:26:11 -0500
commit3c26bc7362c68d6cfdbc853c87ca006ac2e7e539 (patch)
treea252b1f56ac6b7c7ac8aac649b6368c2e6d01b1b /src/Galois
parentf5127ba5bb5c1b932b51f9b3d43a18aa566a6d26 (diff)
assumption lemmas in PointFormats
Diffstat (limited to 'src/Galois')
-rw-r--r--src/Galois/ModularBaseSystem.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v
index 7df44ba7b..138eabd3f 100644
--- a/src/Galois/ModularBaseSystem.v
+++ b/src/Galois/ModularBaseSystem.v
@@ -1,7 +1,7 @@
Require Import Zpower ZArith.
Require Import List.
Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisField.
-Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
+Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
Require Import VerdiTactics.
Local Open Scope Z_scope.