From: Enrico Tassi Date: Mon, 12 May 2008 15:11:14 +0000 (+0000) Subject: height is stored in the reference, no need to fetch the object from the environment X-Git-Tag: make_still_working~5233 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a3df34b044922765655df13d17b18cb11840eb76;p=helm.git height is stored in the reference, no need to fetch the object from the environment --- diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 46a81d620..a825e55d5 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -396,12 +396,12 @@ module Reduction(RS : Strategy) = in aux (k, e, he, tl' @ s) | (_, _, NCic.Const - (NReference.Ref (_,_,NReference.Def) as refer), s) as config -> - let _,_,body,_,_,height = NCicEnvironment.get_checked_def refer in - if delta > height then config else aux (0, [], body, s) + (NReference.Ref (height,_,NReference.Def) as refer), s) as config -> + if delta > height then config else + let _,_,body,_,_,_ = NCicEnvironment.get_checked_def refer in + aux (0, [], body, s) | (_, _, NCic.Const (NReference.Ref - (_,_,NReference.Fix (fixno,recindex)) as refer),s) as config -> - let fixes,_, height = NCicEnvironment.get_checked_fixes_or_cofixes refer in + (height,_,NReference.Fix (fixno,recindex)) as refer),s) as config -> if delta > height then config else (match try Some (RS.from_stack (List.nth s recindex)) @@ -409,6 +409,7 @@ module Reduction(RS : Strategy) = with | None -> config | Some recparam -> + let fixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in match reduce ~delta:0 ~subst context recparam with | (_,_,NCic.Const (NReference.Ref (_,_,NReference.Con _)), _) as c -> let new_s =