diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-06-30 01:57:33 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-06-30 01:57:33 -0400 |
| commit | 518f79958112a93eae30942e62096173c4fb0b28 (patch) | |
| tree | 2107aa0f7d0780c19538a3f76059cf998a999d82 /src/Specific | |
| parent | 2722c6d9b9ee60f01eda70b29ab20785859d385c (diff) | |
add missing import
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/Karatsuba.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Specific/Karatsuba.v b/src/Specific/Karatsuba.v index 97d4149d5..09e014667 100644 --- a/src/Specific/Karatsuba.v +++ b/src/Specific/Karatsuba.v @@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef. Require Import Coq.Lists.List. Import ListNotations. Require Import Crypto.Arithmetic.Core. Import B. Require Import Crypto.Arithmetic.Saturated.Core. +Require Import Crypto.Arithmetic.Saturated.Freeze. Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Import (*Crypto.Util.Tactics*) Crypto.Util.Decidable. Require Import Crypto.Util.LetIn Crypto.Util.ZUtil Crypto.Util.Tactics. |