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
Commit message (
Expand
)
Author
Age
*
Do less reduction in split_in_context
Jason Gross
2018-08-29
*
Improve speed of do_with_exactly_one_hyp tactic
Jason Gross
2018-08-29
*
Add do_with_exactly_one_hyp
Jason Gross
2018-08-29
*
Add specialize_all_ways, fix a proof in src/Compilers/Z/ArithmeticSimplifierI...
Jason Gross
2018-06-26
*
Add fast-path versions of [destruct_head] for unit,bool,True
Jason Gross
2017-12-12
*
Rename run_tactic_as_bool to is_success_run_tactic
Jason Gross
2017-11-26
*
Add Tactics.RunTacticAsConstr
Jason Gross
2017-11-26
*
Add HeadUnderBinders
Jason Gross
2017-11-07
*
Add 8.7-only CacheTerm
Jason Gross
2017-10-18
*
Add CacheTerm
Jason Gross
2017-10-17
*
Add PoseTermWithName
Jason Gross
2017-10-05
*
Make some tactics a bit more powerful
Jason Gross
2017-07-08
*
Add UnfoldArg
Jason Gross
2017-07-08
*
Don't force [Require Import String] for debug msgs
Jason Gross
2017-06-15
*
Add clearbody_all
Jason Gross
2017-06-11
*
More debug info in reification
Jason Gross
2017-05-14
*
s/appcontext/context/
Jason Gross
2017-05-11
*
Add destruct_head'_sum
Jason Gross
2017-04-25
*
Speed up [specialize_by_assumption]
Jason Gross
2017-04-25
*
Fix missing 'by tac' in rewrite_hyp
Jason Gross
2017-04-10
*
Add rewrite_hyp ... by tac
Jason Gross
2017-04-10
*
Make dlet-moving on sigma goals use change
Jason Gross
2017-04-07
*
Faster clear_all tactic
Jason Gross
2017-04-06
*
More vigorous clearing in unify_transformed_rhs_abstract_tac
Jason Gross
2017-04-06
*
Add clear_all
Jason Gross
2017-04-06
*
Don't clutter up typeclass log with cidtac
Jason Gross
2017-04-05
*
Fix transparent assert by to respect names
Jason Gross
2017-04-05
*
Add TransparentAssert
Jason Gross
2017-04-05
*
Remove bad [Local]
Jason Gross
2017-04-05
*
Add Tactics.ChangeInAll
Jason Gross
2017-04-05
*
Add Tactics.MoveLetIn
Jason Gross
2017-04-05
*
Add Tactics.PrintContext
Jason Gross
2017-04-04
*
More fine-grained tactic imports
Jason Gross
2017-04-03
*
Fix parsing issue
Jason Gross
2017-04-03
*
Don't require keeping track of which goals have evars; check that in tactics
Jason Gross
2017-04-03
*
Add UnifyAbstractReflexivity tactics
Jason Gross
2017-04-03
*
Add Tactics.EvarExists
Jason Gross
2017-04-02
*
Split out Tactics.SubstLet
Jason Gross
2017-04-01
*
More compatibility for etransitivity
Jason Gross
2017-03-31
*
Add [etransitivity y], [etransitivity_rev] tactics
Jason Gross
2017-03-31
*
Add split_prod
Jason Gross
2017-03-14
*
Add faster versions of destruct_head_*
Jason Gross
2017-03-14
*
speed up NewBaseystem synthesis
Andres Erbsen
2017-02-23
*
Split off unique {pose,assert}
Jason Gross
2017-01-31
*
Split off some bits of Reflection.Syntax
Jason Gross
2017-01-26
*
Fix infinite loop in destruct_rewrite_sumbool
Jason Gross
2017-01-17
*
More fine-grained util tactic files
Jason Gross
2017-01-17