blob: 7b378c9bff8addfe01aef6746042051f701a1300 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
(** * Generic Tactics *)
Require Export Crypto.Util.FixCoqMistakes.
Require Export Crypto.Util.Tactics.BreakMatch.
Require Export Crypto.Util.Tactics.CacheTerm.
Require Export Crypto.Util.Tactics.ChangeInAll.
Require Export Crypto.Util.Tactics.ClearAll.
Require Export Crypto.Util.Tactics.ClearDuplicates.
Require Export Crypto.Util.Tactics.ClearbodyAll.
Require Export Crypto.Util.Tactics.Contains.
Require Export Crypto.Util.Tactics.ConvoyDestruct.
Require Export Crypto.Util.Tactics.CPSId.
Require Export Crypto.Util.Tactics.DebugPrint.
Require Export Crypto.Util.Tactics.DestructHead.
Require Export Crypto.Util.Tactics.DestructHyps.
Require Export Crypto.Util.Tactics.DestructTrivial.
Require Export Crypto.Util.Tactics.DoWithHyp.
Require Export Crypto.Util.Tactics.ESpecialize.
Require Export Crypto.Util.Tactics.ETransitivity.
Require Export Crypto.Util.Tactics.EvarExists.
Require Export Crypto.Util.Tactics.Forward.
Require Export Crypto.Util.Tactics.GetGoal.
Require Export Crypto.Util.Tactics.HasBody.
Require Export Crypto.Util.Tactics.Head.
Require Export Crypto.Util.Tactics.MoveLetIn.
Require Export Crypto.Util.Tactics.NormalizeCommutativeIdentifier.
Require Export Crypto.Util.Tactics.Not.
Require Export Crypto.Util.Tactics.OnSubterms.
Require Export Crypto.Util.Tactics.PoseTermWithName.
Require Export Crypto.Util.Tactics.PrintContext.
Require Export Crypto.Util.Tactics.Revert.
Require Export Crypto.Util.Tactics.RewriteHyp.
Require Export Crypto.Util.Tactics.SetEvars.
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.
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.
|
