aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics/DestructHead.v
Commit message (Collapse)AuthorAge
* 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]