coq/plugins/dp/vo.itarget, branch master The formal proof system Remove the Dp plugin. 2012-04-17T14:50:28+00:00 gmelquio 2012-04-17T14:50:28+00:00 1028d2f269e7cb46d900f09c31a194531ebd884c 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 
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
Factorisation between Makefile and ocamlbuild systems : .vo to compile are in */*/vo.itarget 2009-12-09T16:45:42+00:00 letouzey 2009-12-09T16:45:42+00:00 cfc9e109a653047b7ca73224525bba67a8c3a571 On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure if you want a partial build, make a specific rule such as theories-light Beware: these vo.itarget should not contain comments. Even if this is legal for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7 
 On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
  if you want a partial build, make a specific rule such as theories-light

 Beware: these vo.itarget should not contain comments. Even if this is legal
  for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7