From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 2 Oct 2008 12:09:40 +0000 (+0000)
Subject: another divergence case patched
X-Git-Tag: make_still_working~4710
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2d8dfec1020c981cc7f75e9bbe3077127ec94394;p=helm.git

another divergence case patched
---

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