From 9a5c5db122becb63c5b72a967ef141bdd3fb5319 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Wed, 17 Nov 2004 17:44:35 +0000
Subject: New command "Print Rewrite HindDb dbname".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/autorewrite.ml  | 14 ++++++++++++++
 tactics/autorewrite.mli |  2 ++
 2 files changed, 16 insertions(+)

(limited to 'tactics')

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index addf30bc4d..ffadc38b44 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -41,6 +41,20 @@ let _ =
       Summary.survive_module = false;
       Summary.survive_section   = false }
 
+let print_rewrite_hintdb bas =
+ try
+  let hints = Stringmap.find bas !rewtab in
+   ppnl (str "Database " ++ str bas ++ (Pp.cut ()) ++
+    prlist_with_sep Pp.cut
+     (fun (c,typ,d,t) ->
+       str (if d then "rewrite -> " else "rewrite <- ") ++
+       Printer.prterm c ++ str " of type " ++ Printer.prterm typ ++
+       str " then use tactic " ++ Pptactic.pr_glob_tactic t) hints)
+ with
+  Not_found -> 
+   errorlabstrm "AutoRewrite" 
+     (str ("Rewriting base "^(bas)^" does not exist"))
+
 type raw_rew_rule = constr * bool * raw_tactic_expr
 
 (* Applies all the rules of one base *)
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index dde6056f87..8b18f23f2c 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -20,3 +20,5 @@ val add_rew_rules : string -> raw_rew_rule list -> unit
 
 (* The AutoRewrite tactic *)
 val autorewrite : tactic -> string list -> tactic
+
+val print_rewrite_hintdb : string -> unit
-- 
cgit v1.2.3