From 92c870913842926076d44bb822ec47f9e0843bc4 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 12 May 2009 13:56:17 +0000 Subject: [PATCH] We only filter the smart candidates w.r.t the signature --- helm/software/components/tactics/auto.ml | 2 ++ 1 file changed, 2 insertions(+) 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 -- 2.39.2