aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic/FunctionalExtensionality.v
Commit message (Expand)AuthorAge
* Axiom-free proof of eta expansion.Gravatar Jasper Hugunin2017-12-11
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* extensionality: Handle dependently-used hypothesesGravatar Jason Gross2016-09-19
* Adding an "extensionality in H" tactic which applies functionalGravatar Hugo Herbelin2016-09-19
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Prove forall extensionalityGravatar Jason Gross2014-08-26
* Adding a dependent version of equal_f, thus fixing #3074.Gravatar ppedrot2013-08-02
* Updating headers.Gravatar herbelin2012-08-08
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Stop using a "Manual Implicit Arguments" flag and support them as soonGravatar msozeau2009-05-27
* Move FunctionalExtensionality to Logic/ (someone please check that theGravatar msozeau2008-12-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 21:06:01 +0000