From f5127ba5bb5c1b932b51f9b3d43a18aa566a6d26 Mon Sep 17 00:00:00 2001 From: varomodt Date: Sat, 9 Jan 2016 13:43:53 -0500 Subject: simple refactor of makefile; comments --- src/Curves/PointFormats.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/Curves/PointFormats.v') diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 7e1fd0f81..1d9a19780 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -1,10 +1,10 @@ -Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ZGaloisField. +Require Import Crypto.Galois.GaloisTheory Crypto.Galois.GaloisField. Require Import Tactics.VerdiTactics. Require Import Logic.Eqdep_dec. Require Import BinNums NArith. Module Type TwistedEdwardsParams (M : Modulus). - Module Export GFDefs := ZGaloisField M. + Module Export GFDefs := GaloisField M. Local Open Scope GF_scope. Axiom char_gt_2 : (1+1) <> 0. Parameter a : GF. @@ -538,7 +538,7 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam End CompleteTwistedEdwardsFacts. Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M. - Module Export GFDefs := ZGaloisField M. + Module Export GFDefs := GaloisField M. Local Open Scope GF_scope. Axiom char_gt_2 : (1+1) <> 0. Definition a := inject (- 1). -- cgit v1.2.3