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 | |
| parent | e72cc12f4fa668f82fe5fd20fa5a20b30f9ecd00 (diff) | |
tuple tooling
Diffstat (limited to 'src/CompleteEdwardsCurve')
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 2 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index e6ec7ab86..f9a866acb 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.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 E. Import Group Ring Field CompleteEdwardsCurve.E. 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. |