From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 2 Oct 2006 15:19:25 +0000 (+0000)
Subject: auto always uses the context (even if paramodulation) to try to close goals left... 
X-Git-Tag: 0.4.95@7852~954
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a828616f9ee55e642b25eece61fda2f67712360f;p=helm.git

auto always uses the context (even if paramodulation) to try to close goals left open by paramod
---

diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml
index dd9e8c186..4b713d464 100644
--- 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