From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 1 Oct 2009 09:49:13 +0000 (+0000)
Subject: instantiate merges tags
X-Git-Tag: make_still_working~3404
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d3ee3b1173e880b33f064551654c96ab4c292363;p=helm.git

instantiate merges tags
---

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index d48dfaf46..5669b1abc 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -328,6 +328,21 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
     (* conjecture: always fail --> occur check *)
     unify test_eq_only metasenv subst context oldt t
   with NCicUtils.Subst_not_found _ -> 
+    let metasenv, tags = 
+      let rec aux = function
+        | NCic.Meta (j,lc) -> 
+            (try 
+              let _, _, t, _ = NCicUtils.lookup_subst j subst in
+              aux (NCicSubstitution.subst_meta lc t)
+            with NCicUtils.Subst_not_found _ -> 
+              let tags', ctx, ty = NCicUtils.lookup_meta j metasenv in
+              let metasenv = List.remove_assoc j metasenv in
+              let tags = tags @ tags' in
+              (j, (tags, ctx, ty)) :: metasenv, tags)
+        | _ -> metasenv, tags
+      in 
+        aux t
+    in
     (* by cumulativity when unify(?,Type_i) 
      * we could ? := Type_j with j <= i... *)
     let subst = (n, (tags, ctx, t, ty)) :: subst in