diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-02-16 18:18:59 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-02-16 18:18:59 -0500 |
| commit | 45a6a17c06f45e81cadf18ef984ec7cdd94c11c1 (patch) | |
| tree | ae821710c13ecd9f07bf8dd4de93adb381691037 /src/Specific/GF25519.v | |
| parent | 7f5205a9133bce6f458d63da4d414a4dfbff7f3b (diff) | |
proved most of point encoding admits, fixed some build system issues (dead imports of PointFormats and Galois things)
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index e716cd244..516efd8b2 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -1,5 +1,5 @@ Require Import ModularArithmetic.PrimeFieldTheorems. -Require Import Galois.BaseSystem Galois.ModularBaseSystem. +Require Import BaseSystem ModularBaseSystem. Require Import List Util.ListUtil. Import ListNotations. Require Import ZArith.ZArith Zpower ZArith Znumtheory. |