aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/FunExt.v
Commit message (Expand)AuthorAge
* extensionality: Handle dependently-used hypothesesGravatar Jason Gross2016-09-19
* Adding an "extensionality in H" tactic which applies functionalGravatar Hugo Herbelin2016-09-19