Passing the correct subst a metasenv when idexing local equations.

diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml
index d65fda22db614749926e73e525a4c1377c9a5e6d..1fa530e782054d30ca02a7da400ed7ef9b0123b3 100644 (file)
--- a/matitaB/components/ng_tactics/nnAuto.ml
+++ b/matitaB/components/ng_tactics/nnAuto.ml
@@ -298,6 +298,7 @@ let index_local_equations eq_cache status =
   let open_goals = head_goals status#stack in
   let open_goal = List.hd open_goals in
   let ngty = get_goalty status open_goal in
+  let _,_,metasenv,subst,_ = status#obj in
   let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
   let c = ref 0 in
   List.fold_left 
@@ -305,12 +306,12 @@ let index_local_equations eq_cache status =
        c:= !c+1;
        let t = NCic.Rel !c in
          try
-           let ty = NCicTypeChecker.typeof status [] [] ctx t in
+           let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
            if is_a_fact status (mk_cic_term ctx ty) then
-             (noprint(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty)));
-              NCicParamod.forward_infer_step status [] [] ctx eq_cache t ty)
+             (noprint(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
+              NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty)
            else 
-             (noprint (lazy ("not a fact: " ^ (status#ppterm ctx [] [] ty)));
+             (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty)));
               eq_cache)
          with 
            | NCicTypeChecker.TypeCheckerFailure _