diff options
author | 2016-07-22 15:33:31 -0700 | |
---|---|---|
committer | 2016-07-22 15:33:31 -0700 | |
commit | 2abb4b5ea3440d478540aad852cfe81e65596189 (patch) | |
tree | 3851f94e613e595bc99da6c932ec99e033694fa3 /src/ModularArithmetic/PrimeFieldTheorems.v | |
parent | 29bb3dd531be45ba7960b34ef759b44436e48905 (diff) | |
parent | 4519b114c66b184611068b2cc9bdad644f4a5a47 (diff) |
Merge pull request #37 from JasonGross/fix-intuition
Redesign intuition, speeding up overall compilation by 20%
Diffstat (limited to 'src/ModularArithmetic/PrimeFieldTheorems.v')
-rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 8d594e8ce..8d47e36ed 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -10,6 +10,7 @@ Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. +Require Export Crypto.Util.FixCoqMistakes. Require Crypto.Algebra. Existing Class prime. |