aboutsummaryrefslogtreecommitdiff
path: root/plugins/pluginsvo.itarget
diff options
context:
space:
mode:
authorgmelquio2012-04-17 14:50:28 +0000
committergmelquio2012-04-17 14:50:28 +0000
commit1028d2f269e7cb46d900f09c31a194531ebd884c (patch)
treebd7cb9781d907caee282b61eb35539e0fa62290f /plugins/pluginsvo.itarget
parenta762421eebc4fe49b1ee2522f3032caa60978f40 (diff)
Remove the Dp plugin.
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
Diffstat (limited to 'plugins/pluginsvo.itarget')
-rw-r--r--plugins/pluginsvo.itarget3
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget
index 2091adf29f..ae2abeb41a 100644
--- a/plugins/pluginsvo.itarget
+++ b/plugins/pluginsvo.itarget
@@ -1,5 +1,4 @@
btauto/vo.otarget
-dp/vo.otarget
field/vo.otarget
fourier/vo.otarget
funind/vo.otarget
@@ -11,4 +10,4 @@ ring/vo.otarget
romega/vo.otarget
rtauto/vo.otarget
setoid_ring/vo.otarget
-extraction/vo.otarget \ No newline at end of file
+extraction/vo.otarget