added hints into Ground

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

1 files changed, 8 insertions, 3 deletions

diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 4d074f67f1..a91b4956c8 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -258,7 +258,7 @@ let create_with_ref_list l depth gl=
 
 open Auto
 
-let create_with_auto_hints depth gl=
+let create_with_auto_hints l depth gl=
   let seqref=ref (empty_seq depth) in
   let f p_a_t =
     match p_a_t.code with
@@ -271,8 +271,13 @@ let create_with_auto_hints depth gl=
 	   with Not_found->())
       | _-> () in
   let g _ l=List.iter f l in
-  let h str hdb=Hint_db.iter g hdb in
-    Util.Stringmap.iter h (!searchtable);
+  let h dbname=
+    let hdb=
+      try
+	Util.Stringmap.find dbname !searchtable 
+      with Not_found-> error ("Ground: "^dbname^" : No such Hint database") in
+      Hint_db.iter g hdb in
+    List.iter h l;
     !seqref
 
 let print_cmap map=