| 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
| 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
in
let small_delta_step is_whd (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
let h1, flex1 = height_of is_whd t1 in
in
let small_delta_step is_whd (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
let h1, flex1 = height_of is_whd t1 in