new internal flags for auto:

[helm.git] / helm / software / components / tactics / declarative.ml

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 15fdbf7254c02ebecfc1744d3e26479d5207806a..be4724b55509124678137083d36c040e519d8dab 100644 (file)
--- 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
 ;;