X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=3e3685063e9497dd2b8bcbfa303af15e739a0f7f;hp=c2a739deaf492ba9396f268b9c89c1891d641e9f;hb=b8a04566e67338e7e5375ff4175277704cd16432;hpb=5cfd68a5d9e73edb40e1cfe021a1426354767aa8

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index c2a739dea..3e3685063 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -1926,13 +1926,17 @@ let candidates_from_ctx univ ctx status =
             let status, res = disambiguate status ctx t `XTNone in 
             let _,res = term_of_cic_term status res (ctx_of res) 
             in Ast.NCic res 
-        in Some (List.map to_Ast l) 
+        in Some ((List.map to_Ast l) @ [Ast.Ident("refl",None); Ast.Ident("sym_eq",None);
+                                        Ast.Ident("trans_eq",None); Ast.Ident("eq_f",None);
+                                        Ast.Ident("eq_f2",None); Ast.Ident("eq_f3",None);
+                                        Ast.Ident("rewrite_r",None); Ast.Ident("rewrite_l",None)
+                                       ])
 
 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 
-    auto_tac' candidates ~local_candidates:false ~use_given_only:true flags ~trace_ref:(ref [])
+    auto_tac' candidates ~local_candidates:false ~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