From: Claudio Sacerdoti Coen Date: Mon, 9 Oct 2006 14:04:31 +0000 (+0000) Subject: Comments updated with new reflections. X-Git-Tag: 0.4.95@7852~922 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=91ab13b3dc451e2abf7fcaf5397320061190c9dd;p=helm.git Comments updated with new reflections. --- diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml index 353662328..1dcbed6d2 100644 --- a/components/cic_unification/cicMetaSubst.ml +++ b/components/cic_unification/cicMetaSubst.ml @@ -625,15 +625,17 @@ let delift n subst context metasenv l t = function C.Rel m -> if m <=k then - C.Rel m (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *) - (*CSC: deliftato la regola per il LetIn *) - (*CSC: FALSO! La regola per il LetIn non lo fa *) + C.Rel m else (try match List.nth context (m-k-1) with Some (_,C.Def (t,_)) -> (*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) | Some (_,C.Decl t) -> C.Rel ((position (m-k) l) + k)