X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality_retrieval.ml;h=962304d41ac8d7c28df9dc9cfffebdd6242aac18;hb=88bdc70aeec4b838517931dd5882a1a26277be1d;hp=e0e92b408db2ad206b032ea7809ca83a90ef17ad;hpb=589ea43c8916e765e43f27b80a2596010527042c;p=helm.git

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 =