X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=130799ea432a7ee1426d7645099c0c40e6a4c5d4;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=e521c6570b8958b092bc86a7020b16a3cad0dc20;hpb=eea144a45e0b58530daeb9a33f79a81a78bd3c9a;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index e521c6570..130799ea4 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -65,7 +65,7 @@ let rec deref subst =
       Cic.Meta(n,l) as t -> 
 	(try 
 	   deref subst
-	     (CicSubstitution.lift_meta 
+	     (CicSubstitution.subst_meta 
 		l (snd (CicUtil.lookup_subst n subst))) 
 	 with 
 	   CicUtil.Subst_not_found _ -> t)
@@ -99,7 +99,7 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
         | C.Meta (i,l) as t->
            (try
              let (_, t') = CicMetaSubst.lookup_subst i subst in
-             aux metasenv subst n context (CicSubstitution.lift_meta l t')
+             aux metasenv subst n context (CicSubstitution.subst_meta l t')
                ugraph
             with CicMetaSubst.SubstNotFound _ ->
               let (subst, metasenv, context, local_context,ugraph1) =
@@ -417,7 +417,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str
         begin
         try
           let (_, oldt) = CicMetaSubst.lookup_subst n subst in
-          let lifted_oldt = S.lift_meta l oldt in
+          let lifted_oldt = S.subst_meta l oldt in
           let ty_lifted_oldt,ugraph1 =
             type_of_aux' metasenv subst context lifted_oldt ugraph
           in
@@ -436,7 +436,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str
             let tyt,ugraph1 = type_of_aux' metasenv subst context t ugraph in
              fo_unif_subst 
               test_equality_only 
-               subst context metasenv tyt (S.lift_meta l meta_type) ugraph1
+               subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
           with AssertFailure _ ->
             (* TODO huge hack!!!!
              * we keep on unifying/refining in the hope that the problem will be
@@ -471,7 +471,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
             (* Unifying the types may have already instantiated n. Let's check *)
             try
              let (_, oldt) = CicMetaSubst.lookup_subst n subst in
-             let lifted_oldt = S.lift_meta l oldt in
+             let lifted_oldt = S.subst_meta l oldt in
               fo_unif_subst_ordered 
                test_equality_only subst context metasenv t lifted_oldt ugraph2
             with
@@ -495,7 +495,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
 	      in
 		fo_unif_subst 
 		  test_equality_only 
-		  subst context metasenv tyt (S.lift_meta l meta_type) ugraph1
+		  subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
             with 
 		UnificationFailure msg 
 	      | Uncertain msg ->
@@ -532,7 +532,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
 	 (* Unifying the types may have already instantiated n. Let's check *)
 	 try
 	   let (_, oldt,_) = CicUtil.lookup_subst n subst in
-	   let lifted_oldt = S.lift_meta l oldt in
+	   let lifted_oldt = S.subst_meta l oldt in
 	     fo_unif_subst_ordered 
 	       test_equality_only subst context metasenv t lifted_oldt ugraph2
 	 with
@@ -634,7 +634,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
 	  *)
             (try 
 	       let (_,t,_) = CicUtil.lookup_subst i subst in
-	       let lifted = S.lift_meta l t in
+	       let lifted = S.subst_meta l t in
                let reduced = beta_reduce (Cic.Appl (lifted::args)) in
 	       fo_unif_subst 
 		 test_equality_only 
@@ -649,7 +649,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
          | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
             (try 
 	       let (_,t,_) = CicUtil.lookup_subst i subst in
-	       let lifted = S.lift_meta l t in
+	       let lifted = S.subst_meta l t in
                let reduced = beta_reduce (Cic.Appl (lifted::args)) in
 	       fo_unif_subst 
 		 test_equality_only