From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Feb 2004 21:26:44 +0000 (+0000)
Subject: We no longer apply the subst to a Meta in force_does_not_occur. In this
X-Git-Tag: V_0_2_3~64
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=39d3fb9782dd5580debfb1e53840906f158e7954;p=helm.git

We no longer apply the subst to a Meta in force_does_not_occur. In this
way we can restrict if something goes wrong.
---

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 22b15f9ee..637c346b0 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -51,24 +51,23 @@ let rec force_does_not_occur subst to_be_restricted t =
     | C.Sort _ as t -> t
     | C.Implicit -> assert false
     | C.Meta (n, l) ->
-        (try
-          aux k (CicSubstitution.lift_meta l (List.assoc n subst))
-        with Not_found ->
-          let l' =
-            let i = ref 0 in
-            List.map
-              (function
-                | None -> None
-                | Some t ->
-                    incr i;
-                    try
-                      Some (aux k t)
-                    with Occur ->
-                      more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
-                      None)
-              l
-          in
-          C.Meta (n, l'))
+       (* we do not retrieve the term associated to ?n in subst since *)
+       (* in this way we can restrict if something goes wrong         *)
+       let l' =
+         let i = ref 0 in
+         List.map
+           (function
+             | None -> None
+             | Some t ->
+                 incr i;
+                 try
+                   Some (aux k t)
+                 with Occur ->
+                   more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
+                   None)
+           l
+       in
+        C.Meta (n, l')
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
     | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
     | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)