From c21e4f8eed450d23b84fde304904bd19b43647da Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 4 Feb 2004 17:32:54 +0000 Subject: [PATCH] delift no longer apply the substitution when a Meta is found. Reason: in this way I can restrict if something goes wrong. --- helm/ocaml/cic_unification/cicMetaSubst.ml | 35 +++++++++++----------- 1 file changed, 17 insertions(+), 18 deletions(-) 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) -- 2.39.2