Changes to declarative tactics, implementation of equality chain

[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 d0ff9c082c1623fc144dedda7849404619471913..21f1e42e81e6e056c67e824780db4d03bfd7afa9 100644 (file)
--- 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