index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Util
/
Tactics
Mode
Name
Size
-rw-r--r--
BreakMatch.v
4948
log
plain
-rw-r--r--
ChangeInAll.v
353
log
plain
-rw-r--r--
ClearAll.v
103
log
plain
-rw-r--r--
ClearDuplicates.v
194
log
plain
-rw-r--r--
ClearbodyAll.v
103
log
plain
-rw-r--r--
Contains.v
283
log
plain
-rw-r--r--
ConvoyDestruct.v
1085
log
plain
-rw-r--r--
DebugPrint.v
2570
log
plain
-rw-r--r--
DestructHead.v
3133
log
plain
-rw-r--r--
DestructHyps.v
1867
log
plain
-rw-r--r--
DestructTrivial.v
204
log
plain
-rw-r--r--
DoWithHyp.v
167
log
plain
-rw-r--r--
ESpecialize.v
132
log
plain
-rw-r--r--
ETransitivity.v
948
log
plain
-rw-r--r--
EvarExists.v
181
log
plain
-rw-r--r--
Forward.v
812
log
plain
-rw-r--r--
GetGoal.v
51
log
plain
-rw-r--r--
Head.v
233
log
plain
-rw-r--r--
MoveLetIn.v
2365
log
plain
-rw-r--r--
Not.v
240
log
plain
-rw-r--r--
OnSubterms.v
226
log
plain
-rw-r--r--
PoseTermWithName.v
297
log
plain
-rw-r--r--
PrintContext.v
420
log
plain
-rw-r--r--
Revert.v
359
log
plain
-rw-r--r--
RewriteHyp.v
7441
log
plain
-rw-r--r--
SetEvars.v
136
log
plain
-rw-r--r--
SetoidSubst.v
928
log
plain
-rw-r--r--
SideConditionsBeforeToAfter.v
799
log
plain
-rw-r--r--
SimplifyProjections.v
1440
log
plain
-rw-r--r--
SimplifyRepeatedIfs.v
688
log
plain
-rw-r--r--
SpecializeBy.v
1369
log
plain
-rw-r--r--
SplitInContext.v
1473
log
plain
-rw-r--r--
SubstEvars.v
109
log
plain
-rw-r--r--
SubstLet.v
71
log
plain
-rw-r--r--
Test.v
223
log
plain
-rw-r--r--
TransparentAssert.v
759
log
plain
-rw-r--r--
UnfoldArg.v
628
log
plain
-rw-r--r--
UnifyAbstractReflexivity.v
2266
log
plain
-rw-r--r--
UniquePose.v
1010
log
plain
-rw-r--r--
VM.v
1298
log
plain