merged changes from the svn fork by me and Enrico

[helm.git] / helm / ocaml / cic_unification / cicMetaSubst.ml

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index d18458e2bb711f486e9f5fe557c6390cffb48c3c..b8784d7172df6c95f1f8b170a62d7ac5dbcdfd31 100644 (file)
--- 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 (CicSubstitution.lift_meta l1 t)
+             deliftaux k (CicSubstitution.subst_meta l1 t)
          with CicUtil.Subst_not_found _ ->
            (* see the top level invariant *)
            if (i = n) then