aboutsummaryrefslogtreecommitdiff
path: root/src/WeierstrassCurve/Pre.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/WeierstrassCurve/Pre.v')
-rw-r--r--src/WeierstrassCurve/Pre.v3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v
index 58ec8b5bf..906a7d1d6 100644
--- a/src/WeierstrassCurve/Pre.v
+++ b/src/WeierstrassCurve/Pre.v
@@ -1,6 +1,7 @@
Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
Require Import Crypto.Algebra Crypto.Algebra.Field.
-Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Notations.
Require Import Crypto.Util.Decidable.
Import BinNums.