aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-03-08 16:09:16 -0500
committerGravatar Jason Gross <jgross@mit.edu>2019-03-08 16:09:16 -0500
commitddd7df2bc75cc2b368aef9bcd02c4344651705e4 (patch)
tree1bebd0af0eb1b1b2c7f3769047e65ac39db2ed95 /src/Util
parent8ba8a4021bc4413fc7fe9996f1748fed7494cd0e (diff)
Fix issue with previous commit
Diffstat (limited to 'src/Util')
-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.