auto always uses the context (even if paramodulation) to try to close goals left...

diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml
index dd9e8c186b5916cabb1b92187d22b5d3b3fb1579..4b713d46492aa10d0ec03316f3a3dedcbcd828bc 100644 (file)
--- a/components/tactics/autoTactic.ml
+++ b/components/tactics/autoTactic.ml
@@ -80,17 +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 = 
+        let cache = 
+          AutoCache.cache_add_context context metasenv AutoCache.cache_empty 
+        in
         if use_only_paramod then (* only paramod *)
-          AutoCache.cache_empty
+          cache
         else
-          let cache = 
-            AutoCache.cache_add_library dbd proof [goal] AutoCache.cache_empty
-          in
-          AutoCache.cache_add_context context metasenv cache
+          AutoCache.cache_add_library dbd proof [goal] 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