aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/functional_principles_proofs.mli
Commit message (Collapse)AuthorAge
* Merge branch v8.6 into trunkGravatar Hugo Herbelin2017-04-22
|\ | | | | | | | | | | Note: I removed what seemed to be dead code in recdef.ml (local_assum and local_def introduced with econstr branch), assuming that this is what should be done.
| * Solving first problem in bug #4306. TO DO : solve the let in problemGravatar Julien Forest2017-04-04
| |
* | Funind API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|/
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
|
* Function now supports puniveresGravatar jforest2015-04-14
|
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵Gravatar letouzey2009-03-20
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7