From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 19 Oct 2006 08:50:31 +0000 (+0000)
Subject: Potential performance improvement + better disambiguation error messages:
X-Git-Tag: 0.4.95@7852~877
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7d748bd1d68d5e47413b411cd8c82ccb5307b0e9;p=helm.git

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.
---

diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml
index 1dcbed6d2..96efe2e3c 100644
--- a/components/cic_unification/cicMetaSubst.ml
+++ b/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