another divergence case patched

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index d60262ccb12adae0cb0267577444076f324e207a..cf8f48053289183b4f8b0b3a153835281376accb 100644 (file)
--- 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