aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics/UnifyAbstractReflexivity.v
Commit message (Collapse)AuthorAge
* More vigorous clearing in unify_transformed_rhs_abstract_tacGravatar Jason Gross2017-04-06
| | | | It makes more evars go away, which were giving [abstract] trouble
* 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