From b880d8ac3206602be68919dd93038e607ae08550 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2009 13:30:38 +0000 Subject: [PATCH 1/1] use prop_only to filter instead of repeting the same function body --- helm/software/components/ng_tactics/nAuto.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) 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), -- 2.39.2