X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTactic.ml;h=4b713d46492aa10d0ec03316f3a3dedcbcd828bc;hb=0663e736012a6bf2af56758181252289e79352d2;hp=bb53991979a93cc385bfdd4292b5053473723dd2;hpb=2eaee49a7ff3ed74598a0db84ce4dbc5bca92380;p=helm.git

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index bb5399197..4b713d464 100644
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -33,11 +33,11 @@
 let bool params name default =
     try 
       let s = List.assoc name params in 
-      if s = "" || s = "1" || s = "true" || s = "yes" then true
-      else if s = "0" || s = "false" || s = "no" then false
+      if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
+      else if s = "0" || s = "false" || s = "no" || s= "off" then false
       else 
         let msg = "Unrecognized value for parameter "^name^"\n" in
-        let msg = msg ^ "Accepted values are 1,true,yes and 0,false,no" in
+        let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
         raise (ProofEngineTypes.Fail (lazy msg))
     with Not_found -> default
 ;; 
@@ -80,12 +80,18 @@ let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
       let _, metasenv, _, _ = proof in
       let _, context, goalty = CicUtil.lookup_meta goal metasenv in
       let cache = 
-        AutoCache.cache_add_library dbd proof [goal] AutoCache.cache_empty
+        let cache = 
+          AutoCache.cache_add_context context metasenv AutoCache.cache_empty 
+        in
+        if use_only_paramod then (* only paramod *)
+          cache
+        else
+          AutoCache.cache_add_library dbd proof [goal] cache
       in 
-      let cache = AutoCache.cache_add_context context metasenv cache in
       let oldmetasenv = metasenv in
       let flags = {
-        AutoTypes.maxdepth = depth;
+        AutoTypes.maxdepth = 
+          if use_only_paramod then 2 else depth;
         AutoTypes.maxwidth = width;
         AutoTypes.timeout = 
           if timeout = 0 then float_of_int timeout