The Blob is not abstracted on the context any more.

[helm.git] / matitaB / components / ng_tactics / nnAuto.ml

diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml
index f3cd17caf1c05b5463f014d7f5d46cd463034754..387e644b0d61a574fac76c2b220a64fd465b7ebd 100644 (file)
--- a/matitaB/components/ng_tactics/nnAuto.ml
+++ b/matitaB/components/ng_tactics/nnAuto.ml
@@ -302,7 +302,7 @@ let index_local_equations eq_cache status =
            let ty = NCicTypeChecker.typeof status [] [] ctx t in
            if is_a_fact status (mk_cic_term ctx ty) then
              (debug_print(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty)));
-              NCicParamod.forward_infer_step eq_cache t ty)
+              NCicParamod.forward_infer_step status [] [] ctx eq_cache t ty)
            else 
              (debug_print (lazy ("not a fact: " ^ (status#ppterm ctx [] [] ty)));
               eq_cache)