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 50558eb39547af4b76ad90e527b8923573a7743a..267f3b10bb1dc30c6fd604f9c86be623a5c13417 100644 (file)
--- 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),