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
*
Add has_body tactic
Jason Gross
2018-12-21
*
Revert "Add inversion_clear tactics"
Jason Gross
2018-12-04
*
Add inversion_clear tactics
Jason Gross
2018-12-04
*
Add a variant of cps_id that pulls the continuation from the lhs
Jason Gross
2018-11-08
*
Add split_contravariant_or
Jason Gross
2018-10-29
*
Improve cps_id tactics, add add_var_types_cps_id, unify_extracted_cps_id tactics
Jason Gross
2018-10-28
*
Fix a bug in ensure_complex_continuation
Jason Gross
2018-10-28
*
Add CPSId tactics
Jason Gross
2018-10-28
*
Rename [normalize_commutative_identifier] file to match tactic name
Jason Gross
2018-10-10
*
Add [normalize_commutative_identifier] tactic
Jason Gross
2018-10-10
*
Add destruct_head_{False,Empty_set}
Jason Gross
2018-09-27
*
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
[next]