diff options
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemOpt.v')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 7c171faf7..a0e1eb06b 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -15,6 +15,7 @@ Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. Require Import Coq.QArith.QArith Coq.QArith.Qround. Require Import Crypto.Tactics.VerdiTactics. +Require Export Crypto.Util.FixCoqMistakes. Local Open Scope Z. Class SubtractionCoefficient (m : Z) (prm : PseudoMersenneBaseParams m) := { @@ -662,4 +663,4 @@ Section Canonicalization. auto using freeze_opt_preserves_rep. Qed. *) -End Canonicalization.
\ No newline at end of file +End Canonicalization. |