1 files changed, 27 insertions, 1 deletions
diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index d46a4a5295..06d3872251 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -16,8 +16,34 @@ open Term
 open Tacmach
 open Tactics
 open Tacticals
-      
+open Libnames
+
+let old_search=ref !Auto.searchtable 
+
+(* I use this solution as a means to know whether hints have changed, 
+but this prevents the GC from collecting the previous table, 
+resulting in some limited space wasting*)
+
+let update_flags ()=
+  if not ( !Auto.searchtable == !old_search ) then
+    begin
+      old_search:=!Auto.searchtable;
+      let predref=ref Names.KNpred.empty in
+      let f p_a_t = 
+	match p_a_t.Auto.code with
+	    Auto.Unfold_nth (ConstRef kn)->
+	      predref:=Names.KNpred.add kn !predref
+	  | _ ->() in
+      let g _ l=List.iter f l in
+      let h _ hdb=Auto.Hint_db.iter g hdb in
+	Util.Stringmap.iter h !Auto.searchtable;
+	red_flags:=
+	Closure.RedFlags.red_add_transparent 
+	  Closure.betaiotazeta (Names.Idpred.full,!predref)
+    end
+
 let ground_tac solver startseq gl=
+  update_flags ();
   let rec toptac skipped seq gl=
     if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
     then Pp.msgnl (Proof_trees.pr_goal (sig_it gl));