From 2d8dfec1020c981cc7f75e9bbe3077127ec94394 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 2 Oct 2008 12:09:40 +0000 Subject: [PATCH] another divergence case patched --- helm/software/components/ng_refiner/nCicUnification.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index d60262ccb..cf8f48053 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -345,7 +345,8 @@ and unify test_eq_only metasenv subst context t1 t2 = | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h, false | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> max_int, true | _ when is_whd -> 0, false - | _ -> max_int, false + | _ -> 0, false (* !!! with max_int we diverge, with 0 we may do too much + reduction *) in let small_delta_step is_whd (_,_,t1,_ as m1) (_,_,t2,_ as m2) = let h1, flex1 = height_of is_whd t1 in -- 2.39.2