From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 21 Nov 2011 11:54:35 +0000 (+0000)
Subject: Passing the correct subst a metasenv when idexing local equations.
X-Git-Tag: make_still_working~2071
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=274921478404b9e0c21d41e02674e1b762fdeaa5;p=helm.git

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 d65fda22d..1fa530e78 100644
--- 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 _