From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 28 Oct 2009 13:30:38 +0000 (+0000)
Subject: use prop_only to filter instead of repeting the same function body
X-Git-Tag: make_still_working~3245
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b880d8ac3206602be68919dd93038e607ae08550;p=helm.git

use prop_only to filter instead of repeting the same function body
---

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 50558eb39..267f3b10b 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -1173,7 +1173,7 @@ let d_goals l =
     aux [] l
 ;;
 let prop_only l =
-  List.filter (function (_,_,P) -> true | _ -> false) l
+  List.filter (function (_,P) -> true | _ -> false) l
 ;;
 
 let rec guess_name name ctx = 
@@ -1374,9 +1374,7 @@ let auto_main flags signature (pos : 'a and_pos) cache =
                   if subgoals = [] then (* this goal has failed *)
                     next_choice (failed pos) cache
                   else
-                    let size_gl l = List.length 
-                      (List.filter (function (_,P) -> true | _ -> false) l)
-                    in
+                    let size_gl l = List.length (prop_only l) in
                     let subtrees = 
                       List.map (fun (_cand,depth_incr,s,gl) ->
                         D(gno,P),