X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fdeclarative.ml;h=be4724b55509124678137083d36c040e519d8dab;hb=87fdda71e8e0dcf886852f70be9a4b3d627b8e9c;hp=15fdbf7254c02ebecfc1744d3e26479d5207806a;hpb=fd93fa0155994b70482e0f07d8e45c238cce835d;p=helm.git

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 15fdbf725..be4724b55 100644
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -27,7 +27,9 @@ type just = [ `Term of Cic.term | `Auto of Auto.auto_params ]
 
 let mk_just ~dbd ~universe =
  function
-    `Auto params -> Tactics.auto ~dbd ~params ~universe
+    `Auto (l,params) -> 
+       Tactics.auto ~dbd 
+       ~params:(l,("skip_trie_filtering","1")::("skip_context","1")::params) ~universe
   | `Term t -> Tactics.apply t
 ;;