From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 4 Feb 2004 17:32:54 +0000 (+0000)
Subject: delift no longer apply the substitution when a Meta is found.
X-Git-Tag: V_0_2_3~65
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c21e4f8eed450d23b84fde304904bd19b43647da;p=helm.git

delift no longer apply the substitution when a Meta is found.
Reason: in this way I can restrict if something goes wrong.
---

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index da9cdb0ac..22b15f9ee 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -259,24 +259,23 @@ let delift n subst context metasenv l t =
             "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
             i (CicPp.ppterm t)))
         else
-          (try
-            deliftaux k (S.lift_meta l (List.assoc i subst))
-          with Not_found ->
-            let rec deliftl j =
-             function
-                [] -> []
-              | None::tl -> None::(deliftl (j+1) tl)
-              | (Some t)::tl ->
-                 let l1' = (deliftl (j+1) tl) in
-                  try
-                   Some (deliftaux k t)::l1'
-                  with
-                     NotInTheList
-                   | MetaSubstFailure _ ->
-                      to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
-            in
-             let l' = deliftl 1 l1 in
-              C.Meta(i,l'))
+         (* I do not consider the term associated to ?i in subst since *)
+         (* in this way I can restrict if something goes wrong.        *)
+          let rec deliftl j =
+           function
+              [] -> []
+            | None::tl -> None::(deliftl (j+1) tl)
+            | (Some t)::tl ->
+               let l1' = (deliftl (j+1) tl) in
+                try
+                 Some (deliftaux k t)::l1'
+                with
+                   NotInTheList
+                 | MetaSubstFailure _ ->
+                    to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
+          in
+           let l' = deliftl 1 l1 in
+            C.Meta(i,l')
      | C.Sort _ as t -> t
      | C.Implicit as t -> t
      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)