X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=fe46e474849861fdfac7fa879d90e2322bcf7af3;hb=a6dd077a2b3e4d0c4395c2ee4cc2e1b6d10ab963;hp=2a7f8c4ae16ed82a9c7800df1345577cae5756fb;hpb=e8236af508187f6446f5af481d545d433628ee00;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 2a7f8c4ae..fe46e4748 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1395,12 +1395,12 @@ and check_metasenv_consistency ~logger ?(subst=[]) metasenv context
      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)
+           (Some (n,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
@@ -1482,15 +1482,15 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 	      ~subst metasenv context canonical_context l ugraph
 	  in
             (* assuming subst is well typed !!!!! *)
-            ((CicSubstitution.lift_meta l ty), ugraph1)
-              (* type_of_aux context (CicSubstitution.lift_meta l term) *)
+            ((CicSubstitution.subst_meta l ty), ugraph1)
+              (* type_of_aux context (CicSubstitution.subst_meta l term) *)
 	with CicUtil.Subst_not_found _ ->
 	  let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
           let ugraph1 = 
 	    check_metasenv_consistency ~logger
 	      ~subst metasenv context canonical_context l ugraph
 	  in
-            ((CicSubstitution.lift_meta l ty),ugraph1))
+            ((CicSubstitution.subst_meta l ty),ugraph1))
       (* TASSI: CONSTRAINTS *)
     | C.Sort (C.Type t) -> 
        let t' = CicUniv.fresh() in