checked in new version of matita from svn

[helm.git] / helm / ocaml / cic_unification / cicUnification.ml

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index e521c6570b8958b092bc86a7020b16a3cad0dc20..130799ea432a7ee1426d7645099c0c40e6a4c5d4 100644 (file)
--- 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