aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/InterpWfRel.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Reflection/InterpWfRel.v')
-rw-r--r--src/Reflection/InterpWfRel.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/InterpWfRel.v b/src/Reflection/InterpWfRel.v
index 59ff53ffe..b827c235a 100644
--- a/src/Reflection/InterpWfRel.v
+++ b/src/Reflection/InterpWfRel.v
@@ -5,7 +5,7 @@ Require Import Crypto.Reflection.Relations.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.Sigma.
Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Notations.
Local Open Scope ctype_scope.
Local Open Scope expr_scope.