From: Enrico Tassi Date: Thu, 12 Oct 2006 16:10:23 +0000 (+0000) Subject: fixed defaultauto behaviour. not the cache is preserveed X-Git-Tag: make_still_working~6754 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=67f28dd5f7a66e93e85badf4cd54e8176cfa6aa8;p=helm.git fixed defaultauto behaviour. not the cache is preserveed --- diff --git a/helm/software/components/tactics/paramodulation/equality_retrieval.ml b/helm/software/components/tactics/paramodulation/equality_retrieval.ml index e0e92b408..962304d41 100644 --- a/helm/software/components/tactics/paramodulation/equality_retrieval.ml +++ b/helm/software/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 =