X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=e42c3ba513ed2d9e1e1993616f1336337f2a9f56;hb=55447138554f33c8588eb836d32ccce2402a09a3;hp=d24c244a75f4f24e26530dd5319229affd2fa0be;hpb=2b80cfd9b2f739a28ea9938c4b1fbb7629839d32;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index d24c244a7..e42c3ba51 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -831,9 +831,13 @@ let pause b = in_pause := b;;
 let cond = Condition.create ();;
 let mutex = Mutex.create ();;
 let hint = ref None;;
+let prune_hint = ref [];;
 
 let step _ = Condition.signal cond;;
 let give_hint n = hint := Some n;;
+let give_prune_hint hint =
+  prune_hint := hint :: !prune_hint
+;;
 
 let check_pause _ =
   if !in_pause then
@@ -1081,7 +1085,7 @@ let equational_case
         assert (maxmeta >= maxm);
         let res' =
           List.map 
-            (fun subst',(_,metasenv,_subst,proof,_, _),open_goals ->
+            (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
                assert_subst_are_disjoint subst subst';
                let subst = subst@subst' in
                let open_goals = 
@@ -1240,7 +1244,18 @@ let prunable menv subst ty todo =
     aux todo
 
 ;;
-
+let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
+  let s = 
+    HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo 
+  in
+  List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
+;;
+let filter_prune_hint l =
+  let prune = !prune_hint in
+  prune_hint := []; (* possible race... *)
+  if prune = [] then l
+  else List.filter (condition_for_prune_hint prune) l
+;;
 let auto_main tables maxm context flags universe cache elems =
   auto_context := context;
   let rec aux tables maxm flags cache (elems : status) =
@@ -1249,8 +1264,9 @@ let auto_main tables maxm context flags universe cache elems =
     auto_status := elems;
     check_pause ();
 *)
+    let elems = filter_prune_hint elems in
     match elems with
-    | (m, s, size, don, todo, fl)::orlist as status when !hint <> None ->
+    | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
         (match !hint with
         | Some i when condition_for_hint i todo ->
             aux tables maxm flags cache orlist
@@ -1755,3 +1771,4 @@ let demodulate_tac ~dbd ~universe =
 let pp_proofterm = Equality.pp_proofterm;;
 
 let revision = "$Revision$";;
+let size_and_depth context metasenv t = 100, 100