From 36809208fa25a494e50004b321fa9a90108ae262 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 Jun 2007 17:12:39 +0000 Subject: [PATCH] sort_new_elems on prop_only --- helm/software/components/tactics/auto.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index e42c3ba51..b439b6cfc 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -1123,8 +1123,8 @@ let try_candidate ;; let sort_new_elems = - List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2) -(* List.sort (fun (_,_,_,l2) (_,_,_,l1) -> List.length l1 - List.length l2) *) + List.sort (fun (_,_,_,l1) (_,_,_,l2) -> + List.length (prop_only l1) - List.length (prop_only l2)) ;; let applicative_case -- 2.39.2