commit by user andrea

[helm.git] / matita / components / ng_tactics / nnAuto.ml

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 9ea4dc03df55518692f62dfdc7b7267f9fdba478..cb42b56912118374391671152644550aba10eef3 100644 (file)
--- 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)));
@@ -1722,7 +1722,7 @@ auto_main flags signature cache depth status: unit =
               let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
               mk_cic_term ctx dty 
             in 
-            prerr_endline ("FAILURE : " ^ ppterm status gty);
+            (*prerr_endline ("FAILURE : " ^ ppterm status gty);*)
             add_to_th newfail failures closegty
           else failures in
         debug_print ~depth (lazy "no more candidates");