X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=21f1e42e81e6e056c67e824780db4d03bfd7afa9;hb=3fab56d1663ba3d5aeb9207612279e0bb0edbb8c;hp=d0ff9c082c1623fc144dedda7849404619471913;hpb=dd627e471392375ca7b6dad78a931a8682e06dbe;p=helm.git

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index d0ff9c082..21f1e42e8 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -1915,7 +1915,7 @@ let auto_lowtac ~params:(univ,flags) status goal =
     let gty = get_goalty status goal in
     let ctx = ctx_of gty in
     let candidates = candidates_from_ctx univ ctx status in 
-    NTactics.exec (auto_tac' candidates ~local_candidates:false ~use_given_only:true flags) status goal
+    auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref:(ref [])
 
 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
     let candidates = candidates_from_ctx univ [] status in