diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-27 14:26:56 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-27 14:26:56 -0400 |
| commit | 6441681c8b861250ab12eb22e8458dff59f84ea3 (patch) | |
| tree | 0bdec302736293c4f1070885e3fdcdc143da49f2 /src/ModularArithmetic | |
| parent | 60b48f8db5afde00fbd3f82b5a06c4b3ce79445c (diff) | |
Fix a missing import in previous commit
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 615bd832b..d8303d1a7 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -7,6 +7,7 @@ Require Import Crypto.ModularArithmetic.ExtendedBaseVector. Require Import Crypto.ModularArithmetic.Pow2Base. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations. Require Import Crypto.ModularArithmetic.ModularBaseSystemList. Require Import Crypto.ModularArithmetic.ModularBaseSystemListProofs. Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. |