aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Util/ListUtil.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index f709e7dd1..ac6575a4f 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -12,6 +12,8 @@ Require Export Crypto.Util.Tactics.BreakMatch.
Require Export Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Crypto.Util.Tactics.RewriteHyp.
+Import ListNotations.
+Local Open Scope list_scope.
Scheme Equality for list.