instantiate merges tags

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index d48dfaf460a4967a02aada9d8f7ee5f8bdecd03c..5669b1abcd9bd4d500e220ae4c1d462fc067961f 100644 (file)
--- 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