diff options
| author | sacerdot | 2004-11-17 17:44:35 +0000 |
|---|---|---|
| committer | sacerdot | 2004-11-17 17:44:35 +0000 |
| commit | 9a5c5db122becb63c5b72a967ef141bdd3fb5319 (patch) | |
| tree | 456513517718198461fabae4e96242348aeeab13 /tactics | |
| parent | 85500252f0e8c0d2b2cceb2418bcadadbbc5cfd0 (diff) | |
New command "Print Rewrite HindDb dbname".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/autorewrite.ml | 14 | ||||
| -rw-r--r-- | tactics/autorewrite.mli | 2 |
2 files changed, 16 insertions, 0 deletions
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 |