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 436d309c7..5f748e0f6 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -16,6 +16,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) := { @@ -702,4 +703,4 @@ Section Canonicalization. auto using freeze_opt_preserves_rep. Qed. *) -End Canonicalization.
\ No newline at end of file +End Canonicalization. |