X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=cb42b56912118374391671152644550aba10eef3;hb=ea12b736382320bcedad780ec0eb522ff5cc35a5;hp=23ad46494dbc1f92b6b03a781174f00af168eb34;hpb=cef076c6fbd4ceec7c460414cf4421611457188d;p=helm.git

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 23ad46494..cb42b5691 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -1668,7 +1668,7 @@ auto_main flags signature cache depth status: unit =
            NCicParamod.is_equation status metasenv subst ctx ty in
         (* if the goal is an equality we artificially raise its depth up to
            flags.maxdepth - 1 *)
-        if (not flags.last && is_eq && (depth < (flags.maxdepth -1))) then
+        if (not flags.last && is_eq && (depth < (flags.maxdepth -2))) then
         (* for efficiency reasons, in this case we severely cripple the
            search depth *)
           (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));