From 67f28dd5f7a66e93e85badf4cd54e8176cfa6aa8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Oct 2006 16:10:23 +0000 Subject: [PATCH] fixed defaultauto behaviour. not the cache is preserveed --- .../components/tactics/paramodulation/equality_retrieval.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 = -- 2.39.5