to avoid a case of divergence small_delta_step checks if terms are flexible and

gives 0 as delta

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 16178bd3b3e8af51a21591322c6071074a75afca..d60262ccb12adae0cb0267577444076f324e207a 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -338,21 +338,22 @@ and unify test_eq_only metasenv subst context t1 t2 =
        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
        | _ -> raise (uncert_exc metasenv subst context t1 t2)
     in
-    let height_of = function
+    let height_of is_whd = function
      | NCic.Const (Ref.Ref (_,Ref.Def h)) 
      | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) 
      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_) 
-     | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
-     | NCic.Meta _ -> max_int
-     | _ -> 0
+     | 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
     in
-    let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = 
-      let h1 = height_of t1 in 
-      let h2 = height_of t2 in
+    let small_delta_step is_whd (_,_,t1,_ as m1) (_,_,t2,_ as m2) = 
+      let h1, flex1 = height_of is_whd t1 in 
+      let h2, flex2 = height_of is_whd t2 in
       let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
       NCicReduction.reduce_machine ~delta ~subst context m1,
       NCicReduction.reduce_machine ~delta ~subst context m2,
-      delta
+      if is_whd && flex1 && flex2 then 0 else delta
     in
     let rec unif_machines metasenv subst = function
       | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
@@ -365,7 +366,7 @@ and unify test_eq_only metasenv subst context t1 t2 =
               try
                 let t1 = NCicReduction.from_stack t1 in
                 let t2 = NCicReduction.from_stack t2 in
-                unif_machines metasenv subst (small_delta_step t1 t2)
+                unif_machines metasenv subst (small_delta_step true t1 t2)
               with UnificationFailure _ | Uncertain _ when not b ->
                 metasenv, subst
           in
@@ -389,11 +390,10 @@ and unify test_eq_only metasenv subst context t1 t2 =
           unif_machines metasenv subst (red m1,red m2,delta)
      in
      try fo_unif test_eq_only metasenv subst t1 t2
-     with UnificationFailure msg |Uncertain msg as exn 
-     when not (flexible [t1;t2]) -> 
+     with UnificationFailure msg | Uncertain msg as exn -> 
        try 
          unif_machines metasenv subst 
-          (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
+          (small_delta_step false (0,[],t1,[]) (0,[],t2,[]))
        with 
        | UnificationFailure _ -> raise (UnificationFailure msg)
        | Uncertain _ -> raise exn