From dc0eae6607f2b299deeeb1a2c4e145e7a6d40629 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Dec 2008 13:54:37 +0000 Subject: [PATCH] fixed a bug, it used to report o wrong is_normal bit in case of match --- helm/software/components/ng_kernel/nCicReduction.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 7dbe379e4..3b0823395 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -114,7 +114,9 @@ module Reduction(RS : Strategy) = struct aux (k, e, he, tl' @ s) | (_, _, C.Const (Ref.Ref (_,Ref.Def height) as refer), s) as config -> - if delta >= height then config, false else + if delta >= height then + config, false + else let _,_,body,_,_,_ = NCicEnvironment.get_checked_def refer in aux (0, [], body, s) | (_, _, C.Const (Ref.Ref (_, @@ -154,13 +156,15 @@ module Reduction(RS : Strategy) = struct c | config -> config in - (match decofix (fst (reduce ~delta:0 ~subst context (k,e,term,[]))) with + let match_head = k,e,term,[] in + let reduced,_ = reduce ~delta:0 ~subst context match_head in + (match decofix reduced with | (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,_))),[]) -> aux (k, e, List.nth pl (j-1), s) | (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,lno))), s')-> let _,params = HExtlib.split_nth lno s' in aux (k, e, List.nth pl (j-1), params@s) - | _ -> config,true) + | _ -> config,reduced == match_head) in aux ;; -- 2.39.2