diff options
Diffstat (limited to 'src/Arithmetic/ModularArithmeticTheorems.v')
| -rw-r--r-- | src/Arithmetic/ModularArithmeticTheorems.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v index 666dd54eb..d1fcd80b9 100644 --- a/src/Arithmetic/ModularArithmeticTheorems.v +++ b/src/Arithmetic/ModularArithmeticTheorems.v @@ -8,7 +8,9 @@ Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac. Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.ScalarMult. Require Crypto.Algebra.Ring Crypto.Algebra.Field. -Require Import Crypto.Util.Decidable Crypto.Util.ZUtil. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Export Crypto.Util.FixCoqMistakes. Module F. |