diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-03-30 18:30:29 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-03-30 18:30:29 -0400 |
| commit | ce1a0e8508f53481138362f14581193b7394552b (patch) | |
| tree | 18f27142e59fbf2a006500db8280d9ddcfbc8669 /src/Specific/GF25519.v | |
| parent | 019c80c66cd4da0f7e3f6469bf1fe3ede11c7a12 (diff) | |
| parent | d819eeb7bd87746b62f6a6398f6ad69edb89a5ff (diff) | |
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 795c360ed..14a7332e7 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -1,12 +1,12 @@ -Require Import ModularArithmetic.PrimeFieldTheorems. -Require Import ModularArithmetic.PseudoMersenneBaseRep. -Require Import ModularArithmetic.PseudoMersenneBaseParams. -Require Import BaseSystem ModularBaseSystem. -Require Import List Util.ListUtil. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseRep. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.BaseSystem Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Coq.Lists.List Crypto.Util.ListUtil. Import ListNotations. -Require Import ZArith.ZArith Zpower ZArith Znumtheory. -Require Import QArith.QArith QArith.Qround. -Require Import VerdiTactics. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coq.QArith.QArith Coq.QArith.Qround. +Require Import Crypto.Tactics.VerdiTactics. Close Scope Q. Local Open Scope Z. |