aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics/DestructHead.v
Commit message (Collapse)AuthorAge
* Revert "Add inversion_clear tactics"Gravatar Jason Gross2018-12-04
| | | | | | This reverts commit e6044c2fe0cc7b5662076bb1f26342a4d590132e. Actually not needed; the tactics already clear the relevant hypotheses.
* Add inversion_clear tacticsGravatar Jason Gross2018-12-04
|
* Add destruct_head_{False,Empty_set}Gravatar Jason Gross2018-09-27
|
* Add fast-path versions of [destruct_head] for unit,bool,TrueGravatar Jason Gross2017-12-12
|
* Add destruct_head'_sumGravatar Jason Gross2017-04-25
|
* Add faster versions of destruct_head_*Gravatar Jason Gross2017-03-14
| | | | Sometimes, it's a performance bottleneck
* More fine-grained util tactic filesGravatar Jason Gross2017-01-17
Also, add [split_and]