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 06844a2092951e81d13363c0c8cd98bd228ebcba..45cab35026a4dd196ee765c4cd742cf3918da073 100644 (file)
--- 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)