aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/CommonSubexpressionElimination.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Reflection/CommonSubexpressionElimination.v')
-rw-r--r--src/Reflection/CommonSubexpressionElimination.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/CommonSubexpressionElimination.v b/src/Reflection/CommonSubexpressionElimination.v
index 433c45aa8..6d3921aa6 100644
--- a/src/Reflection/CommonSubexpressionElimination.v
+++ b/src/Reflection/CommonSubexpressionElimination.v
@@ -2,7 +2,7 @@
Require Import Coq.Lists.List.
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Util.Tactics Crypto.Util.Bool.
+Require Import (*Crypto.Util.Tactics*) Crypto.Util.Bool.
Local Open Scope list_scope.