From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 contrib/dp/g_dp.ml4 | 43 ++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 42 insertions(+), 1 deletion(-)

(limited to 'contrib/dp/g_dp.ml4')

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
+
-- 
cgit v1.2.3