aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics/DoWithHyp.v
Commit message (Collapse)AuthorAge
* Improve speed of do_with_exactly_one_hyp tacticGravatar Jason Gross2018-08-29
| | | | | We assume that there are many hypotheses, and that running [tac] is just as fast to succeed as to fail.
* Add do_with_exactly_one_hypGravatar Jason Gross2018-08-29
|
* Split off some bits of Reflection.SyntaxGravatar Jason Gross2017-01-26
Also split off some bits of Util.Tactics