From 9369ab9136d5726669b30f3598f2e433fba438d9 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 12 Nov 2004 18:13:17 +0000
Subject: [PATCH] Fixed an hidden occur check problem: when a Meta is being
 delifted, apply substitution on the fly and delift the result. Previously we
 did not recursively check the instantiation of the Meta.

---
 helm/ocaml/cic_unification/cicMetaSubst.ml | 56 ++++++++++++----------
 1 file changed, 30 insertions(+), 26 deletions(-)

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index db63ff568..ae5299dc5 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -655,32 +655,36 @@ let delift n subst context metasenv l t =
         in
          C.Var (uri,exp_named_subst')
      | C.Meta (i, l1) as t -> 
-         (* see the top level invariant *)
-	 if (i = n) then 
-          raise (MetaSubstFailure (sprintf
-            "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
-            i (ppterm subst t))) 
-        else
-          begin
-         (* 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')
-	  end
+         (try
+           let (_,t,_) = CicUtil.lookup_subst i subst in
+           deliftaux k t
+         with CicUtil.Subst_not_found _ ->
+           (* see the top level invariant *)
+           if (i = n) then 
+            raise (MetaSubstFailure (sprintf
+              "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
+              i (ppterm subst t))) 
+          else
+            begin
+           (* 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')
+            end)
      | C.Sort _ as t -> t
      | C.Implicit _ as t -> t
      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
-- 
2.39.2