- | 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
+(* | NCic.Rel _ -> 1, WRONG *)
+ | _ when is_whd -> 0, false
+ | _ -> max_int, false