From 0f80463f3b4a23940b5cffcb09e1b2e28154d14f Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 12 May 2013 16:17:23 +0000
Subject: 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
---
 tactics/extratactics.ml4 | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index af04dcacbc..5a8fc3bbb8 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
 
 (**********************************************************************)
-- 
cgit v1.2.3