diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-07-08 16:17:02 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-07-08 16:17:02 -0400 |
| commit | 59dec7e5b97b447e91a8d86440848f4c5d74c93f (patch) | |
| tree | f577b6f4b71c1f426823e9257af3c0db94b29a80 /src/Arithmetic/PrimeFieldTheorems.v | |
| parent | 86772a8a67e246ba93c708bdb0459f2f39edb966 (diff) | |
More fine-grained tactics imports
Diffstat (limited to 'src/Arithmetic/PrimeFieldTheorems.v')
| -rw-r--r-- | src/Arithmetic/PrimeFieldTheorems.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Arithmetic/PrimeFieldTheorems.v b/src/Arithmetic/PrimeFieldTheorems.v index 842313b93..a4305a849 100644 --- a/src/Arithmetic/PrimeFieldTheorems.v +++ b/src/Arithmetic/PrimeFieldTheorems.v @@ -12,6 +12,7 @@ Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Decidable. Require Export Crypto.Util.FixCoqMistakes. +Require Import Crypto.Util.Tactics.BreakMatch. Require Crypto.Algebra.Hierarchy Crypto.Algebra.Field. Existing Class prime. |