aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic/FunctionalExtensionality.v
AgeCommit message (Collapse)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-27Stop using a "Manual Implicit Arguments" flag and support them as soonmsozeau
as they are used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12148 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-16Move FunctionalExtensionality to Logic/ (someone please check that themsozeau
doc is ok). Rework the .v files in Program accordingly, adding some documentation and proper headers. Integrate the development of an elimination principle for measured functions in Program/Wf by Eelis van der Weegen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11686 85f007b7-540e-0410-9357-904b9bb8a0f7