X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=4873481ed9b7df99b93f06170483cad0e9563f6d;hp=21f1e42e81e6e056c67e824780db4d03bfd7afa9;hb=90e823f96159811d88b275df9c3ec9a4c40ff816;hpb=489639a3c319d0349a9c864fd0eeaf659daa3d3f

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 21f1e42e8..4873481ed 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -323,9 +323,6 @@ let index_local_equations eq_cache ?(flag=false) status =
 ;;
 
 let index_local_equations2 eq_cache status open_goal lemmas ?(flag=false) nohyps =
- if flag then
-  NCicParamod.empty_state
- else begin
   noprint (lazy "indexing equations");
   let eq_cache,lemmas =
    match lemmas with
@@ -361,7 +358,6 @@ let index_local_equations2 eq_cache status open_goal lemmas ?(flag=false) nohyps
            | NCicTypeChecker.TypeCheckerFailure _
            | NCicTypeChecker.AssertFailure _ -> eq_cache)
     eq_cache lemmas
- end
 ;;
 
 let fast_eq_check_tac ~params s = 
@@ -1911,7 +1907,7 @@ let candidates_from_ctx univ ctx status =
             in Ast.NCic res 
         in Some (List.map to_Ast l) 
 
-let auto_lowtac ~params:(univ,flags) status goal =
+let auto_lowtac ~params:(univ,flags as params) status goal =
     let gty = get_goalty status goal in
     let ctx = ctx_of gty in
     let candidates = candidates_from_ctx univ ctx status in