Granting wish #3014:

  Hint Rewrite should allow multiple databases.

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

1 files changed, 10 insertions, 8 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index af04dcacb..5a8fc3bbb 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -250,21 +250,23 @@ TACTIC EXTEND rewrite_star
 (**********************************************************************)
 (* Hint Rewrite                                                       *)
 
-let add_rewrite_hint name ort t lcsr =
+let add_rewrite_hint bases ort t lcsr =
   let env = Global.env() and sigma = Evd.empty in
   let f c = Constrexpr_ops.constr_loc c, Constrintern.interp_constr sigma env c, ort, t in
-  add_rew_rules name (List.map f lcsr)
+  let eqs = List.map f lcsr in
+  let add_hints base = add_rew_rules base eqs in
+  List.iter add_hints bases
 
 VERNAC COMMAND EXTEND HintRewrite
-  [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident(b) ] ->
-  [ add_rewrite_hint b o (Tacexpr.TacId []) l ]
+  [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
+  [ add_rewrite_hint bl o (Tacexpr.TacId []) l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
-    ":" preident(b) ] ->
-  [ add_rewrite_hint b o t l ]
+    ":" preident_list(bl) ] ->
+  [ add_rewrite_hint bl o t l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
-  [ add_rewrite_hint "core" o (Tacexpr.TacId []) l ]
+  [ add_rewrite_hint ["core"] o (Tacexpr.TacId []) l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
-  [ add_rewrite_hint "core" o t l ]
+  [ add_rewrite_hint ["core"] o t l ]
 END
 
 (**********************************************************************)