diff options
| author |  varomodt <varomodt@localhost.localdomain> | 2016-01-09 13:43:53 -0500 |
|---|---|---|
| committer | varomodt <varomodt@localhost.localdomain> | 2016-01-09 13:43:53 -0500 |
| commit | f5127ba5bb5c1b932b51f9b3d43a18aa566a6d26 (patch) | |
| tree | 44938bc996c9604322a84391399743af9993a5c0 /src/Curves/PointFormats.v | |
| parent | bb4c8e7d281279eb9aeb44c5d0de5be1d022028c (diff) | |
simple refactor of makefile; comments
Diffstat (limited to 'src/Curves/PointFormats.v')
| -rw-r--r-- | src/Curves/PointFormats.v | 6 |
1 files changed, 3 insertions, 3 deletions
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). |