From ce51a8e4b5c03178a08b7cd0e5bd34bae2fdf4a0 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 20 Jun 2016 02:00:55 -0400 Subject: tuple tooling --- src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 2 +- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'src/CompleteEdwardsCurve') 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. -- cgit v1.2.3