| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2012-04-17 | Remove the Dp plugin. | gmelquio | |
| Why2 has not been maintained for the last few years and the Why3 plugin should be a suitable replacement in most cases. Removed tactics: simplify, ergo, yices, cvc3, z3, cvcl, harvey, zenon, gwhy. Removed commands: Dp_hint, Dp_timeout, Dp_prelude, Dp_predefined, Dp_debug, Dp_trace. Note that the "admit" tactic was actually provided by the Dp plugin. It has been moved to extratactics.ml4. Ported from v8.4 r15186. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15189 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2011-02-03 | Dp: another fix suggested by Virgile Prevosto | letouzey | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13811 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2009-11-10 | use only why-dp, support for z3 | marche | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12491 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2009-09-07 | ajout CVC3; ajout traduction des reels | marche | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12309 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2009-03-20 | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵ | letouzey | |
| user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |