merged changes from the svn fork by me and Enrico

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 2a7f8c4ae16ed82a9c7800df1345577cae5756fb..fe46e474849861fdfac7fa879d90e2322bcf7af3 100644 (file)
--- 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