From 274921478404b9e0c21d41e02674e1b762fdeaa5 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 21 Nov 2011 11:54:35 +0000 Subject: [PATCH] Passing the correct subst a metasenv when idexing local equations. --- matitaB/components/ng_tactics/nnAuto.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) 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 _ -- 2.39.2