aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics
Commit message (Expand)AuthorAge
* Add constr_fail and constr_fail_withGravatar Jason Gross2019-03-31
* Remove GlobalTacticalsGravatar Jason Gross2019-03-08
* Fix grepeat tacticGravatar Jason Gross2019-03-08
* Fix gprogress tacticalGravatar Jason Gross2019-03-08
* Add some gtacticsGravatar Jason Gross2019-03-08
* Add has_body tacticGravatar Jason Gross2018-12-21
* Revert "Add inversion_clear tactics"Gravatar Jason Gross2018-12-04
* Add inversion_clear tacticsGravatar Jason Gross2018-12-04
* Add a variant of cps_id that pulls the continuation from the lhsGravatar Jason Gross2018-11-08
* Add split_contravariant_orGravatar Jason Gross2018-10-29
* Improve cps_id tactics, add add_var_types_cps_id, unify_extracted_cps_id tacticsGravatar Jason Gross2018-10-28
* Fix a bug in ensure_complex_continuationGravatar Jason Gross2018-10-28
* Add CPSId tacticsGravatar Jason Gross2018-10-28
* Rename [normalize_commutative_identifier] file to match tactic nameGravatar Jason Gross2018-10-10
* Add [normalize_commutative_identifier] tacticGravatar Jason Gross2018-10-10
* Add destruct_head_{False,Empty_set}Gravatar Jason Gross2018-09-27
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 18:20:45 +0000