Better (and more localized) error message for sort_of_prod.

[helm.git] / helm / software / components / tactics / paramodulation / equality_retrieval.ml

diff --git a/helm/software/components/tactics/paramodulation/equality_retrieval.ml b/helm/software/components/tactics/paramodulation/equality_retrieval.ml
index e0e92b408db2ad206b032ea7809ca83a90ef17ad..962304d41ac8d7c28df9dc9cfffebdd6242aac18 100644 (file)
--- 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 =