New command "Print Rewrite HindDb dbname".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7

12 files changed, 33 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 2f72a3a5f3..6862c81914 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,11 @@
 Changes from V8.0
 =================
 
+Vernacular commands
+
+- Added "Print Rewrite HintDb" to print the content of a DB used by
+  autorewrite (doc TODO)
+
 Gallina
 
 - Added disjunctive patterns in match-with patterns
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 88ffb2bcee..dfe64d2274 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -124,6 +124,7 @@ and ct_COMMAND =
   | CT_print_graph
   | CT_print_hint of ct_ID_OPT
   | CT_print_hintdb of ct_ID_OR_STAR
+  | CT_print_rewrite_hintdb of ct_ID
   | CT_print_id of ct_ID
   | CT_print_implicit of ct_ID
   | CT_print_loadpath
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 48047cf96f..ebad140808 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -418,6 +418,9 @@ and fCOMMAND = function
 | CT_print_hintdb(x1) ->
    fID_OR_STAR x1;
    fNODE "print_hintdb" 1
+| CT_print_rewrite_hintdb(x1) ->
+   fID x1;
+   fNODE "print_rewrite_hintdb" 1
 | CT_print_id(x1) ->
    fID x1;
    fNODE "print_id" 1
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index a997e30958..b0a0f4977c 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1768,6 +1768,8 @@ let rec xlate_vernac =
 	| PrintHintDb -> CT_print_hintdb (CT_coerce_STAR_to_ID_OR_STAR CT_star)
 	| PrintHintDbName id -> 
 	    CT_print_hintdb (CT_coerce_ID_to_ID_OR_STAR (CT_ident id))
+	| PrintRewriteHintDbName id -> 
+	    CT_print_rewrite_hintdb (CT_ident id)
 	| PrintHint id ->
 	    CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_qualid_to_ct_ID id))
 	| PrintHintGoal -> CT_print_hint ctv_ID_OPT_NONE
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 0176ccf852..0e16a18d46 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -174,6 +174,7 @@ let state_preserving = [
   "Print Module Type";
   "Print Modules";
   "Print Proof";
+  "Print Rewrite HintDb";
   "Print Setoids";
   "Print Scope";
   "Print Scopes.";
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index cd4213aa73..79b0e26fc1 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -197,6 +197,7 @@ GEXTEND Gram
       | IDENT "Hint"; qid = global -> PrintHint qid
       | IDENT "Hint"; "*" -> PrintHintDb
       | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
+      | IDENT "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s
       | IDENT "Scopes" -> PrintScopes
       | IDENT "Scope"; s = IDENT -> PrintScope s
       | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index dafd6b3cad..2346ae0849 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -594,6 +594,7 @@ GEXTEND Gram
       | IDENT "Hint"; qid = global -> PrintHint qid
       | IDENT "Hint"; "*" -> PrintHintDb
       | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
+      | IDENT "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s
       | IDENT "Setoids" -> PrintSetoids
       | IDENT "Scopes" -> PrintScopes
       | IDENT "Scope"; s = IDENT -> PrintScope s
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
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3c8dd414eb..a7df137858 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -930,6 +930,7 @@ let vernac_print = function
   | PrintHint qid -> Auto.print_hint_ref (Nametab.global qid)
   | PrintHintGoal -> Auto.print_applicable_hint ()
   | PrintHintDbName s -> Auto.print_hint_db_by_name s
+  | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s
   | PrintHintDb -> Auto.print_searchtable ()
   | PrintSetoids -> Setoid_replace.print_setoids()
   | PrintScopes ->
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 031cc98a26..afcc361f83 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -55,6 +55,7 @@ type printable =
   | PrintHint of reference
   | PrintHintGoal
   | PrintHintDbName of string
+  | PrintRewriteHintDbName of string
   | PrintHintDb
   | PrintSetoids
   | PrintScopes
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 4441b0b52d..e16e59d0ef 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -1022,6 +1022,7 @@ let rec pr_vernac = function
 	| PrintHint qid -> str"Print Hint" ++ spc() ++ pr_reference qid
 	| PrintHintDb -> str"Print Hint *"
 	| PrintHintDbName s -> str"Print HintDb" ++ spc() ++ str s
+	| PrintRewriteHintDbName s -> str"Print Rewrite HintDb" ++ spc() ++ str s
 	| PrintUniverses fopt -> str"Dump Universes" ++ pr_opt str fopt
 	| PrintName qid -> str"Print" ++ spc()  ++ pr_reference qid
 	| PrintLocalContext -> assert false