From a3df34b044922765655df13d17b18cb11840eb76 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 12 May 2008 15:11:14 +0000 Subject: [PATCH] height is stored in the reference, no need to fetch the object from the environment --- helm/software/components/ng_kernel/nCicReduction.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) 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 = -- 2.39.2