diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/dp/g_dp.ml4 | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/dp/g_dp.ml4')
-rw-r--r-- | plugins/dp/g_dp.ml4 | 79 |
1 files changed, 79 insertions, 0 deletions
diff --git a/plugins/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4 new file mode 100644 index 00000000..82f86cd8 --- /dev/null +++ b/plugins/dp/g_dp.ml4 @@ -0,0 +1,79 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* $Id$ *) + +open Dp + +TACTIC EXTEND Simplify + [ "simplify" ] -> [ simplify ] +END + +TACTIC EXTEND Ergo + [ "ergo" ] -> [ ergo ] +END + +TACTIC EXTEND Yices + [ "yices" ] -> [ yices ] +END + +TACTIC EXTEND CVC3 + [ "cvc3" ] -> [ cvc3 ] +END + +TACTIC EXTEND Z3 + [ "z3" ] -> [ z3 ] +END + +TACTIC EXTEND CVCLite + [ "cvcl" ] -> [ cvc_lite ] +END + +TACTIC EXTEND Harvey + [ "harvey" ] -> [ harvey ] +END + +TACTIC EXTEND Zenon + [ "zenon" ] -> [ zenon ] +END + +TACTIC EXTEND Gwhy + [ "gwhy" ] -> [ gwhy ] +END + +(* should be part of basic tactics syntax *) +TACTIC EXTEND admit + [ "admit" ] -> [ Tactics.admit_as_an_axiom ] +END + +VERNAC COMMAND EXTEND Dp_hint + [ "Dp_hint" ne_global_list(l) ] -> [ dp_hint l ] +END + +VERNAC COMMAND EXTEND Dp_timeout +| [ "Dp_timeout" natural(n) ] -> [ dp_timeout n ] +END + +VERNAC COMMAND EXTEND Dp_prelude +| [ "Dp_prelude" string_list(l) ] -> [ dp_prelude l ] +END + +VERNAC COMMAND EXTEND Dp_predefined +| [ "Dp_predefined" global(g) "=>" string(s) ] -> [ dp_predefined g s ] +END + +VERNAC COMMAND EXTEND Dp_debug +| [ "Dp_debug" ] -> [ dp_debug true; Dp_zenon.set_debug true ] +END + +VERNAC COMMAND EXTEND Dp_trace +| [ "Dp_trace" ] -> [ dp_trace true ] +END + |