aboutsummaryrefslogtreecommitdiff
path: root/src/Algebra/Field_test.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Algebra/Field_test.v')
-rw-r--r--src/Algebra/Field_test.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Algebra/Field_test.v b/src/Algebra/Field_test.v
index 3bdd65089..522010d5c 100644
--- a/src/Algebra/Field_test.v
+++ b/src/Algebra/Field_test.v
@@ -1,3 +1,4 @@
+Require Import Coq.PArith.BinPosDef.
Require Import Crypto.Util.Decidable Crypto.Util.Notations.
Require Import Crypto.Algebra.Ring Crypto.Algebra.Field.