From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 28 Apr 2009 16:23:14 +0000 (+0000)
Subject: depenalization of smart apply inside auto, that is now much faster
X-Git-Tag: make_still_working~4041
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d4b31ea5ca7c7dd3344cb284a89fac22312834cf;p=helm.git

depenalization of smart apply inside auto, that is now much faster
---

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)