From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 15 Oct 2008 22:24:01 +0000 (+0000)
Subject: subst_meta was missing
X-Git-Tag: make_still_working~4683
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c45a4837a6f3c9d6af14b2057389442bf6d2f32f;p=helm.git

subst_meta was missing
---

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 10bc29a62..24ab7b4af 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -174,6 +174,7 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
   try
     let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
     let oldt = NCicSubstitution.subst_meta lc oldt in
+    let t = NCicSubstitution.subst_meta lc t in
     (* conjecture: always fail --> occur check *)
     unify test_eq_only metasenv subst context oldt t
   with NCicUtils.Subst_not_found _ -> 
@@ -181,7 +182,7 @@ and instantiate test_eq_only metasenv subst context n lc t swap =
      * we could ? := Type_j with j <= i... *)
     let subst = (n, (name, ctx, t, ty)) :: subst in
     pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
-      ~metasenv ~subst ~context:ctx (NCicSubstitution.subst_meta lc t)));
+      ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
     let metasenv = 
       List.filter (fun (m,_) -> not (n = m)) metasenv 
     in