From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 12 Oct 2006 16:10:23 +0000 (+0000)
Subject: fixed defaultauto behaviour. not the cache is preserveed
X-Git-Tag: 0.4.95@7852~895
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3826abcbbb8b8bca2d7de88e8c4e6b4bce5a930b;p=helm.git

fixed defaultauto behaviour. not the cache is preserveed
---

diff --git a/components/tactics/paramodulation/equality_retrieval.ml b/components/tactics/paramodulation/equality_retrieval.ml
index e0e92b408..962304d41 100644
--- a/components/tactics/paramodulation/equality_retrieval.ml
+++ b/components/tactics/paramodulation/equality_retrieval.ml
@@ -136,7 +136,7 @@ let equations_blacklist = UriManager.UriSet.empty;;
 (*****************************************************************)
 exception AutoFailure of AutoCache.cache * int
 
-let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;; 
+let default_auto maxm _ _ _ c _ = [],c,maxm ;; 
 
 let close_hypothesis_of_term context metasenv oldnewmeta term cache auto fast = 
   let head, metasenv, args, newmeta =