| Some bo -> aux (ctx,bo))
| (name, src)::ctx, (NCic.Appl args as bo)
when HExtlib.list_last args = NCic.Rel 1 ->
- let args, _ = HExtlib.split_nth (List.length args - 1) args in
+ let args, _ = HExtlib.split_nth "NU 1" (List.length args - 1) args in
(match delift_if_not_occur (NCic.Appl args) with
| None -> aux (ctx,NCic.Lambda(name,src, bo))
| Some bo -> aux (ctx,bo))
let relevance = match r1 with
| Ref.Ref (_,Ref.Con (_,_,lno)) ->
let relevance =
- try snd (HExtlib.split_nth lno relevance)
+ try snd (HExtlib.split_nth "NU 2" lno relevance)
with Failure _ -> []
in
HExtlib.mk_list false lno @ relevance