merged changes from the svn fork by me and Enrico

[helm.git] / helm / ocaml / cic_omdoc / doubleTypeInference.ml

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
index 128da869b72a142b8cb914c80f68a02a221952ff..6bfced57e2ad69ed44982773a8bdb85961372ff1 100644 (file)
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -367,9 +367,9 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
            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)))::
+               (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 (_,C.Def (_,Some _)))::_ -> assert false
@@ -398,7 +398,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           in
            let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
             (* Checks suppressed *)
-            CicSubstitution.lift_meta l ty
+            CicSubstitution.subst_meta l ty
      | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
          C.Sort (C.Type (CicUniv.fresh()))
      | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *)