X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautomationCache.ml;h=34bb3efdfe4ee836b783a0f0d4f1b7000b2665c8;hb=25564c06c570e5ab9be455904c0b381842f8d4c4;hp=7d8e7d129d9032406c0e9f30cf6dcbb90fcfd0e3;hpb=91f0c0e84bfe6bf22e960d466e16f7260a2882ee;p=helm.git

diff --git a/helm/software/components/tactics/automationCache.ml b/helm/software/components/tactics/automationCache.ml
index 7d8e7d129..34bb3efdf 100644
--- a/helm/software/components/tactics/automationCache.ml
+++ b/helm/software/components/tactics/automationCache.ml
@@ -67,7 +67,7 @@ let add_term_to_active cache metasenv subst context t ty_opt =
             ~subst metasenv context t CicUniv.oblivion_ugraph
         in
         let bag, head, metasenv, args =
-          Equality.saturate_term bag metasenv context ty
+          Equality.saturate_term bag metasenv subst context ty
         in
         let mes = CicUtil.metas_of_term (Cic.Appl (head::t::args)) in
         let t = if args = [] then t else Cic.Appl (t:: args) in