aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic/FunctionalExtensionality.v
AgeCommit message (Collapse)Author
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