aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/FunExt.v
AgeCommit message (Expand)Author
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2016-09-19extensionality: Handle dependently-used hypothesesJason Gross
2016-09-19Adding an "extensionality in H" tactic which applies functionalHugo Herbelin