From c3f967910eca5648fd69886166c66ddd49d92b54 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 9 Mar 2008 16:53:38 +0000 Subject: [PATCH] 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! --- helm/software/components/cic_unification/cicMetaSubst.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml index f082fc230..070a07c93 100644 --- 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")) -- 2.39.2