aboutsummaryrefslogtreecommitdiff
path: root/src/MontgomeryX.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/MontgomeryX.v')
-rw-r--r--src/MontgomeryX.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/MontgomeryX.v b/src/MontgomeryX.v
index b3e9a5ae8..0bc611473 100644
--- a/src/MontgomeryX.v
+++ b/src/MontgomeryX.v
@@ -1,6 +1,6 @@
Require Import Crypto.Algebra Crypto.Algebra.Field.
Require Import Crypto.Util.GlobalSettings Crypto.Util.Notations.
-Require Import Crypto.Util.Tactics Crypto.Util.Sum Crypto.Util.Prod.
+Require Import (*Crypto.Util.Tactics*) Crypto.Util.Sum Crypto.Util.Prod.
Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurveTheorems.
Module M.