aboutsummaryrefslogtreecommitdiff
path: root/src/CompleteEdwardsCurve/ExtendedCoordinates.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/CompleteEdwardsCurve/ExtendedCoordinates.v')
-rw-r--r--src/CompleteEdwardsCurve/ExtendedCoordinates.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 4a352c738..fe0e732a8 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -6,7 +6,7 @@ Require Import Coq.Logic.Eqdep_dec.
Require Import Crypto.Tactics.VerdiTactics.
Require Import Coq.Classes.Morphisms.
Require Import Relation_Definitions.
-Require Import Crypto.Util.Fieldwise.
+Require Import Crypto.Util.Tuple.
Module Extended.
Section ExtendedCoordinates.