apply and auto.equational_case call saturation.solve_narrowing

[helm.git] / helm / software / components / tactics / automationCache.ml

diff --git a/helm/software/components/tactics/automationCache.ml b/helm/software/components/tactics/automationCache.ml
index 7d8e7d129d9032406c0e9f30cf6dcbb90fcfd0e3..34bb3efdfe4ee836b783a0f0d4f1b7000b2665c8 100644 (file)
--- 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