diff options
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 |