X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=b8784d7172df6c95f1f8b170a62d7ac5dbcdfd31;hb=5580474eef409dc311f2db6e31974b4783450b23;hp=ae5299dc588a11bd8fb59ef660fff725ebe0c5fb;hpb=9369ab9136d5726669b30f3598f2e433fba438d9;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index ae5299dc5..b8784d717 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -83,7 +83,7 @@ let rec deref subst =
       Cic.Meta(n,l) as t -> 
 	(try 
 	   deref subst
-	     (CicSubstitution.lift_meta 
+	     (CicSubstitution.subst_meta 
 		l (third (CicUtil.lookup_subst n subst))) 
 	 with 
 	   CicUtil.Subst_not_found _ -> t)
@@ -183,7 +183,7 @@ let apply_subst_gen ~appl_fun subst term =
     | C.Meta (i, l) -> 
         (try
           let (_, t,_) = lookup_subst i subst in
-          um_aux (S.lift_meta l t)
+          um_aux (S.subst_meta l t)
         with CicUtil.Subst_not_found _ -> 
 	  (* unconstrained variable, i.e. free in subst*)
           let l' =
@@ -657,7 +657,7 @@ let delift n subst context metasenv l t =
      | C.Meta (i, l1) as t -> 
          (try
            let (_,t,_) = CicUtil.lookup_subst i subst in
-           deliftaux k t
+             deliftaux k (CicSubstitution.subst_meta l1 t)
          with CicUtil.Subst_not_found _ ->
            (* see the top level invariant *)
            if (i = n) then