diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-06-20 02:00:55 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-06-20 02:00:55 -0400 |
commit | ce51a8e4b5c03178a08b7cd0e5bd34bae2fdf4a0 (patch) | |
tree | 11f3dead685c79e67f16d10480955a7df7c88ba7 /src/CompleteEdwardsCurve/ExtendedCoordinates.v | |
parent | e72cc12f4fa668f82fe5fd20fa5a20b30f9ecd00 (diff) |
tuple tooling
Diffstat (limited to 'src/CompleteEdwardsCurve/ExtendedCoordinates.v')
-rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 2 |
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. |