diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-25 22:41:08 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-25 22:41:08 -0400 |
| commit | a8836bda7dc57933098fe5d513a52221591252b0 (patch) | |
| tree | f86ddaf0f075ae357a852be408c51e9d6a34200b /src/ModularArithmetic/ModularBaseSystemList.v | |
| parent | 4c73b7273c5fae67154ad9dd8bd3a719e4fbcf5f (diff) | |
Fix 8.4 build.
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemList.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemList.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemList.v b/src/ModularArithmetic/ModularBaseSystemList.v index cbab03d6a..b46429fcc 100644 --- a/src/ModularArithmetic/ModularBaseSystemList.v +++ b/src/ModularArithmetic/ModularBaseSystemList.v @@ -1,4 +1,5 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. +Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Coq.Lists.List. Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. |