diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-03 15:23:17 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-03 15:23:17 -0400 |
| commit | efbc255af154acdecb5217f80d64dd23e2421923 (patch) | |
| tree | b55da77f06705c3632894d75302325eb6fc0354d /src | |
| parent | 9009ddf4261bbf489874c4619a8c0397eb3f989d (diff) | |
Be more fine-grained in WeierstrassCurveTheorems imports
We don't need to rebuild it every time we add a new Tactics/ file
Diffstat (limited to 'src')
| -rw-r--r-- | src/WeierstrassCurve/WeierstrassCurveTheorems.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/WeierstrassCurve/WeierstrassCurveTheorems.v b/src/WeierstrassCurve/WeierstrassCurveTheorems.v index b9f7458b0..59b87305d 100644 --- a/src/WeierstrassCurve/WeierstrassCurveTheorems.v +++ b/src/WeierstrassCurve/WeierstrassCurveTheorems.v @@ -2,8 +2,8 @@ Require Import Coq.Numbers.BinNums. Require Import Coq.Classes.Morphisms. Require Import Crypto.Spec.WeierstrassCurve. Require Import Crypto.Algebra Crypto.Algebra.Field. -Require Import Crypto.Util.Decidable Crypto.Util.Tactics. -Require Import BinPos. +Require Import Crypto.Util.Decidable Crypto.Util.Tactics.DestructHead Crypto.Util.Tactics.BreakMatch. +Require Import Coq.PArith.BinPos. Module W. Section W. |