merged changes from the svn fork by me and Enrico

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

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 8401ad5ade42339c3a24b56b06627273d10440cd..621834e3326dd4fbc124dfbec1138433ed9e42e2 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -224,17 +224,17 @@ and type_of_aux' metasenv context t ugraph =
                   canonical_context l ugraph 
                in
                 (* trust or check ??? *)
-                C.Meta (n,l'),CicSubstitution.lift_meta l' ty, 
+                C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
                    subst', metasenv', ugraph1
                   (* type_of_aux subst metasenv 
-                     context (CicSubstitution.lift_meta l term) *)
+                     context (CicSubstitution.subst_meta l term) *)
              with CicUtil.Subst_not_found _ ->
                let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
                let l',subst',metasenv', ugraph1 =
                 check_metasenv_consistency n subst metasenv context
                   canonical_context l ugraph
                in
-                C.Meta (n,l'),CicSubstitution.lift_meta l' ty, 
+                C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
                    subst', metasenv',ugraph1)
        | C.Sort (C.Type tno) -> 
             let tno' = CicUniv.fresh() in 
@@ -605,14 +605,14 @@ and type_of_aux' metasenv context t ugraph =
        function
             [] -> []
          | (Some (n,C.Decl t))::tl ->
-              (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+              (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
          | (Some (n,C.Def (t,None)))::tl ->
-              (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
+              (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
          | None::tl -> None::(aux (i+1) tl)
          | (Some (n,C.Def (t,Some ty)))::tl ->
               (Some (n,
-                    C.Def ((S.lift_meta l (S.lift i t)),
-                           Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
+                    C.Def ((S.subst_meta l (S.lift i t)),
+                           Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
       in
        aux 1 canonical_context 
     in