aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2018-06-26 15:01:10 -0400
committerGravatar Jason Gross <jagro@google.com>2018-06-26 15:01:10 -0400
commit19fd81bfae1d8fad0b31a8415e4259c11ab80c0a (patch)
tree5aab218ad86e39f47cbec46728ad778329c30063 /src/Util/Tactics.v
parentbdb73e3541400f7197fb683eb5f140c62d749ad8 (diff)
Add specialize_all_ways, fix a proof in src/Compilers/Z/ArithmeticSimplifierInterp.v
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 5a2bca803..95b4a29fc 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -31,6 +31,7 @@ Require Export Crypto.Util.Tactics.SetoidSubst.
Require Export Crypto.Util.Tactics.SideConditionsBeforeToAfter.
Require Export Crypto.Util.Tactics.SimplifyProjections.
Require Export Crypto.Util.Tactics.SimplifyRepeatedIfs.
+Require Export Crypto.Util.Tactics.SpecializeAllWays.
Require Export Crypto.Util.Tactics.SpecializeBy.
Require Export Crypto.Util.Tactics.SplitInContext.
Require Export Crypto.Util.Tactics.SubstEvars.