From: Enrico Tassi Date: Fri, 19 Sep 2008 16:44:36 +0000 (+0000) Subject: snapshot X-Git-Tag: make_still_working~4755 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2a5fa3d7b64f23c060a2e6a2a4b87c6f277ddfae;p=helm.git snapshot --- diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index b5a4646ba..c7d66dd06 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -382,35 +382,18 @@ let delift metasenv subst context n l t = (metasenv, subst), NCic.Meta(newmeta,l1)) | t -> NCicUtils.map_term_fold_a (fun _ k -> k+1) k aux ms t in - aux 0 (metasenv,subst) t -;; - -(* - in - let res = - try - deliftaux 0 t - with - NotInTheList -> + try aux 0 (metasenv,subst) t + with NotInTheList -> (* This is the case where we fail even first order unification. *) (* The reason is that our delift function is weaker than first *) (* order (in the sense of alpha-conversion). See comment above *) (* related to the delift function. *) -(* debug_print (lazy "First Order UnificationFailure during delift") ; -debug_print(lazy (sprintf - "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" - (ppterm subst t) - (String.concat "; " - (List.map - (function Some t -> ppterm subst t | None -> "_") l - )))); *) - let msg = (lazy (sprintf - "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" - (ppterm ~metasenv subst t) - (String.concat "; " - (List.map - (function Some t -> ppterm ~metasenv subst t | None -> "_") - l)))) + let msg = (lazy (Printf.sprintf + ("Error trying to abstract %s over [%s]: the algorithm only tried to "^^ + "abstract over bound variables") (NCicPp.ppterm ~metasenv ~subst + ~context t) (String.concat "; " (List.map (NCicPp.ppterm ~metasenv + ~subst ~context) (let shift, lc = l in List.map (NCicSubstitution.lift + shift) (NCicUtils.expand_local_context lc)))))) in if List.exists @@ -421,11 +404,7 @@ debug_print(lazy (sprintf raise (Uncertain msg) else raise (MetaSubstFailure msg) - in - let (metasenv, subst) = restrict subst !to_be_restricted metasenv in - res, metasenv, subst ;; -*) (* (* delifts a term t of n levels strating from k, that is changes (Rel m)