From 982a3285c2f8b554ceae11b46c204bf61bfba1ed Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 19 Oct 2006 08:50:31 +0000 Subject: [PATCH] Potential performance improvement + better disambiguation error messages: the delift functions used to raise Uncertain every time it failed; now it raises Failure when the local context contains no Metas (that means that for every future subst it will not contain new Rels). Note: if we are working up to conversion (I do not think so), we should check that the local context is Meta-closed, that is a weaker check. --- .../components/cic_unification/cicMetaSubst.ml | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml index 1dcbed6d2..96efe2e3c 100644 --- a/helm/software/components/cic_unification/cicMetaSubst.ml +++ b/helm/software/components/cic_unification/cicMetaSubst.ml @@ -740,13 +740,24 @@ debug_print(lazy (sprintf (List.map (function Some t -> ppterm subst t | None -> "_") l )))); *) - raise (Uncertain (lazy (sprintf + let msg = (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))))) + l)))) + in + if + (*CSC: WARNING: if we are working up to reduction (I do not think so), + the following test should be replaced with "all the terms in l are + meta-closed" *) + not + (List.exists (function Some (Cic.Meta _) -> true | _ -> false ) l) + then + raise (MetaSubstFailure msg) + else + raise (Uncertain msg) in let (metasenv, subst) = restrict subst !to_be_restricted metasenv in res, metasenv, subst -- 2.39.2