Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | [API] Remove `open API` in ml files in favor of `-open API` flag. | Emilio Jesus Gallego Arias | 2017-07-17 |
| | |||
* | Removing Proof_type from the API. | Pierre-Marie Pédrot | 2017-06-16 |
| | | | | | | | Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead. | ||
* | Remove (useless) aliases from the API. | Matej Košík | 2017-06-10 |
| | |||
* | Put all plugins behind an "API". | Matej Kosik | 2017-06-07 |
| | |||
* | Remove unused [open] statements | Gaetan Gilbert | 2017-04-27 |
| | |||
* | Merge branch v8.6 into trunk | Hugo Herbelin | 2017-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 problem | Julien Forest | 2017-04-04 |
| | | |||
* | | Funind API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 |
|/ | |||
* | Fix some typos. | Guillaume Melquiond | 2015-12-07 |
| | |||
* | Function now supports puniveres | jforest | 2015-04-14 |
| | |||
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-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 ↵ | letouzey | 2009-03-20 |
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7 |