From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 12 May 2009 13:56:17 +0000 (+0000)
Subject: We only filter the smart candidates w.r.t the signature
X-Git-Tag: make_still_working~3989
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=92c870913842926076d44bb822ec47f9e0843bc4;p=helm.git

We only filter the smart candidates w.r.t the signature
---

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 53120a44d..81d5c6f4c 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -1714,7 +1714,9 @@ let smart_applicative_case dbd
     (lazy ("smart_candidates" ^ " = " ^ 
              (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
   debug_print debug_msg;
+(* we only filter the smart candidates since they could be too many 
   let candidates = List.filter (only signature context metasenv) candidates in
+*)
   let smart_candidates = 
     List.filter (only signature context metasenv) smart_candidates 
   in