aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic/FunctionalExtensionality.v
AgeCommit message (Expand)Author
2020-12-15Modify Logic/FunctionalExtensionality.v to compile with -mangle-namesJasper Hugunin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-11Axiom-free proof of eta expansion.Jasper Hugunin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-09-19extensionality: Handle dependently-used hypothesesJason Gross
2016-09-19Adding an "extensionality in H" tactic which applies functionalHugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-08-26Prove forall extensionalityJason Gross
2013-08-02Adding a dependent version of equal_f, thus fixing #3074.ppedrot
2012-08-08Updating headers.herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-05-27Stop using a "Manual Implicit Arguments" flag and support them as soonmsozeau
2008-12-16Move FunctionalExtensionality to Logic/ (someone please check that themsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:19:31 +0000