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/ModularArithmetic/ModularBaseSystem.v | |
| parent | 019c80c66cd4da0f7e3f6469bf1fe3ede11c7a12 (diff) | |
| parent | d819eeb7bd87746b62f6a6398f6ad69edb89a5ff (diff) | |
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystem.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 2bfcdcf0b..f63bfbb1c 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -1,8 +1,12 @@ -Require Import Zpower ZArith. -Require Import List. -Require Import Crypto.Util.ListUtil. +Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.BaseSystem Crypto.ModularArithmetic.PseudoMersenneBaseParams Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.Tactics.VerdiTactics. Local Open Scope Z_scope. Section PseudoMersenneBase. |