Potentially (and, at least sometimes, actually) big performance improvement:

let-in were always zeta-expanded during delifting. As a result, implicit,
in a context with definitions, were always refined with a type that was well
typed, but only up to (potentially expensive) reduction!

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index f082fc23092d6aa1074e54426dbb4ad2994ac170..070a07c932dc7e24fbab11fecc278650fffccc31 100644 (file)
--- a/helm/software/components/cic_unification/cicMetaSubst.ml
+++ b/helm/software/components/cic_unification/cicMetaSubst.ml
@@ -653,13 +653,17 @@ let delift n subst context metasenv l t =
            (try
             match List.nth context (m-k-1) with
                Some (_,C.Def (t,_)) ->
+                (try
+                  C.Rel ((position (m-k) l) + k)
+                 with
+                  NotInTheList ->
                 (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
                 (*CSC: first order unification. Does it help or does it harm? *)
                 (*CSC: ANSWER: it hurts performances since it is possible to  *)
                 (*CSC: have an exponential explosion of the size of the proof.*)
                 (*CSC: However, without this bit of reduction some "apply" in *)
                 (*CSC: the library fail (e.g. nat/nth_prime.ma).              *)
-                deliftaux k (S.lift m t)
+                  deliftaux k (S.lift m t))
              | Some (_,C.Decl t) ->
                 C.Rel ((position (m-k) l) + k)
              | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))