From d4b31ea5ca7c7dd3344cb284a89fac22312834cf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 28 Apr 2009 16:23:14 +0000 Subject: [PATCH] depenalization of smart apply inside auto, that is now much faster --- helm/software/components/tactics/auto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 06844a209..45cab3502 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -1749,7 +1749,7 @@ let smart_applicative_case dbd (fun (tables,elems) cand -> match try_smart_candidate dbd goalty - tables subst fake_proof goalno 1 context cand + tables subst fake_proof goalno depth context cand with | None, tables -> tables, elems | Some x, tables -> tables, x::elems) -- 2.39.2