aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-07-08 15:59:53 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-07-08 16:01:19 -0400
commit5aa6b0a6b2ac0561125716710662adab6ad6f333 (patch)
treedcd50d5c9e51bca63566e10a48a824f0e197e42f /src/Util/Tactics.v
parentc13b59e4e416b308f709bf5e901f29580fb04f5a (diff)
Add UnfoldArg
Diffstat (limited to 'src/Util/Tactics.v')
-rw-r--r--src/Util/Tactics.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 4d39d4954..af75b4f50 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -35,6 +35,7 @@ Require Export Crypto.Util.Tactics.SubstEvars.
Require Export Crypto.Util.Tactics.SubstLet.
Require Export Crypto.Util.Tactics.Test.
Require Export Crypto.Util.Tactics.TransparentAssert.
+Require Export Crypto.Util.Tactics.UnfoldArg.
Require Export Crypto.Util.Tactics.UnifyAbstractReflexivity.
Require Export Crypto.Util.Tactics.UniquePose.
Require Export Crypto.Util.Tactics.VM.