diff options
Diffstat (limited to 'contrib/dp/g_dp.ml4')
| -rw-r--r-- | contrib/dp/g_dp.ml4 | 43 |
1 files changed, 42 insertions, 1 deletions
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4 index eb7fb73b..99bcf477 100644 --- a/contrib/dp/g_dp.ml4 +++ b/contrib/dp/g_dp.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: g_dp.ml4 7165 2005-06-24 12:56:46Z coq $ *) +(* $Id: g_dp.ml4 10924 2008-05-13 14:01:11Z filliatr $ *) open Dp @@ -16,6 +16,14 @@ TACTIC EXTEND Simplify [ "simplify" ] -> [ simplify ] END +TACTIC EXTEND Ergo + [ "ergo" ] -> [ ergo ] +END + +TACTIC EXTEND Yices + [ "yices" ] -> [ yices ] +END + TACTIC EXTEND CVCLite [ "cvcl" ] -> [ cvc_lite ] END @@ -28,6 +36,18 @@ TACTIC EXTEND Zenon [ "zenon" ] -> [ zenon ] END +TACTIC EXTEND Gwhy + [ "gwhy" ] -> [ gwhy ] +END + +TACTIC EXTEND Gappa_internal + [ "gappa_internal" ] -> [ Dp_gappa.gappa_internal ] +END + +TACTIC EXTEND Gappa + [ "gappa" ] -> [ Dp_gappa.gappa ] +END + (* should be part of basic tactics syntax *) TACTIC EXTEND admit [ "admit" ] -> [ Tactics.admit_as_an_axiom ] @@ -36,3 +56,24 @@ 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 + |