From: Claudio Sacerdoti Coen Date: Mon, 9 Oct 2006 14:04:31 +0000 (+0000) Subject: Comments updated with new reflections. X-Git-Tag: make_still_working~6781 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0a3f0acfde37361bb12f53aeb89988ab188233d6;p=helm.git Comments updated with new reflections. --- diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml index 353662328..1dcbed6d2 100644 --- a/helm/software/components/cic_unification/cicMetaSubst.ml +++ b/helm/software/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)