X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=621834e3326dd4fbc124dfbec1138433ed9e42e2;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=8401ad5ade42339c3a24b56b06627273d10440cd;hpb=07b55308c296ec8537a176d829d161a975306e58;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 8401ad5ad..621834e33 100644
--- 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