aboutsummaryrefslogtreecommitdiff
path: root/src/Fancy/Barrett256.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Fancy/Barrett256.v')
-rw-r--r--src/Fancy/Barrett256.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Fancy/Barrett256.v b/src/Fancy/Barrett256.v
index 0474e6e07..2911ab788 100644
--- a/src/Fancy/Barrett256.v
+++ b/src/Fancy/Barrett256.v
@@ -2,7 +2,6 @@ Require Import Coq.Bool.Bool.
Require Import Coq.derive.Derive.
Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
Require Import Coq.Lists.List. Import ListNotations.
-Require Import Crypto.Arithmetic.
Require Import Crypto.COperationSpecifications. Import COperationSpecifications.BarrettReduction.
Require Import Crypto.Fancy.Compiler.
Require Import Crypto.Fancy.Prod.