From 39d3fb9782dd5580debfb1e53840906f158e7954 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Feb 2004 21:26:44 +0000 Subject: [PATCH] We no longer apply the subst to a Meta in force_does_not_occur. In this way we 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 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) -- 2.39.2