X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=d371409d2ecac8587947476abcba11087074d43d;hp=3ac6040dc3e79995405e2000732e71a1df8b67cb;hb=89fc31fc5cc01e8860cf67a8e096c24125370d31;hpb=f38fd769279794d0ca73c8945eac30e8b42e59be

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 3ac6040dc..d371409d2 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -1925,11 +1925,14 @@ 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) @ [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)
-                                       ])
+        in Some (List.map to_Ast l)
+(* FG: adding these lemmas to (List.map to_Ast l) slows auto very much in some cases 
+                                    @ [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) status goal =
     let gty = get_goalty status goal in