diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-25 21:06:20 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-25 21:06:20 -0400 |
| commit | 4c73b7273c5fae67154ad9dd8bd3a719e4fbcf5f (patch) | |
| tree | f2e60ad282447023ff59330e77ee588657e77e97 /src/ModularArithmetic/ModularBaseSystemOpt.v | |
| parent | 39a6c95de8a900c859726d875cc40ea96298d31b (diff) | |
| parent | b9312acc45407a58d07e19e407e9575d427dd6c3 (diff) | |
Merge branch 'master' of github.com:mit-plv/fiat-crypto
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. |