aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics
Commit message (Expand)AuthorAge
* Do less reduction in split_in_contextGravatar Jason Gross2018-08-29
* Improve speed of do_with_exactly_one_hyp tacticGravatar Jason Gross2018-08-29
* Add do_with_exactly_one_hypGravatar Jason Gross2018-08-29
* Add specialize_all_ways, fix a proof in src/Compilers/Z/ArithmeticSimplifierI...Gravatar Jason Gross2018-06-26
* Add fast-path versions of [destruct_head] for unit,bool,TrueGravatar Jason Gross2017-12-12
* Rename run_tactic_as_bool to is_success_run_tacticGravatar Jason Gross2017-11-26
* Add Tactics.RunTacticAsConstrGravatar Jason Gross2017-11-26
* Add HeadUnderBindersGravatar Jason Gross2017-11-07
* Add 8.7-only CacheTermGravatar Jason Gross2017-10-18
* Add CacheTermGravatar Jason Gross2017-10-17
* Add PoseTermWithNameGravatar Jason Gross2017-10-05
* Make some tactics a bit more powerfulGravatar Jason Gross2017-07-08
* Add UnfoldArgGravatar Jason Gross2017-07-08
* Don't force [Require Import String] for debug msgsGravatar Jason Gross2017-06-15
* Add clearbody_allGravatar Jason Gross2017-06-11
* More debug info in reificationGravatar Jason Gross2017-05-14
* s/appcontext/context/Gravatar Jason Gross2017-05-11
* Add destruct_head'_sumGravatar Jason Gross2017-04-25
* Speed up [specialize_by_assumption]Gravatar Jason Gross2017-04-25
* Fix missing 'by tac' in rewrite_hypGravatar Jason Gross2017-04-10
* Add rewrite_hyp ... by tacGravatar Jason Gross2017-04-10
* Make dlet-moving on sigma goals use changeGravatar Jason Gross2017-04-07
* Faster clear_all tacticGravatar Jason Gross2017-04-06
* More vigorous clearing in unify_transformed_rhs_abstract_tacGravatar Jason Gross2017-04-06
* Add clear_allGravatar Jason Gross2017-04-06
* Don't clutter up typeclass log with cidtacGravatar Jason Gross2017-04-05
* Fix transparent assert by to respect namesGravatar Jason Gross2017-04-05
* Add TransparentAssertGravatar Jason Gross2017-04-05
* Remove bad [Local]Gravatar Jason Gross2017-04-05
* Add Tactics.ChangeInAllGravatar Jason Gross2017-04-05
* Add Tactics.MoveLetInGravatar Jason Gross2017-04-05
* Add Tactics.PrintContextGravatar Jason Gross2017-04-04
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Fix parsing issueGravatar Jason Gross2017-04-03
* Don't require keeping track of which goals have evars; check that in tacticsGravatar Jason Gross2017-04-03
* Add UnifyAbstractReflexivity tacticsGravatar Jason Gross2017-04-03
* Add Tactics.EvarExistsGravatar Jason Gross2017-04-02
* Split out Tactics.SubstLetGravatar Jason Gross2017-04-01
* More compatibility for etransitivityGravatar Jason Gross2017-03-31
* Add [etransitivity y], [etransitivity_rev] tacticsGravatar Jason Gross2017-03-31
* Add split_prodGravatar Jason Gross2017-03-14
* Add faster versions of destruct_head_*Gravatar Jason Gross2017-03-14
* speed up NewBaseystem synthesisGravatar Andres Erbsen2017-02-23
* Split off unique {pose,assert}Gravatar Jason Gross2017-01-31
* Split off some bits of Reflection.SyntaxGravatar Jason Gross2017-01-26
* Fix infinite loop in destruct_rewrite_sumboolGravatar Jason Gross2017-01-17
* More fine-grained util tactic filesGravatar Jason Gross2017-01-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-11 10:57:37 +0000