From 3826abcbbb8b8bca2d7de88e8c4e6b4bce5a930b 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/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 = -- 2.39.2