| (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,_))),[]) ->
aux (k, e, List.nth pl (j-1), s)
| (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,lno))), s')->
- let _,params = HExtlib.split_nth "NR 1" lno s' in
+ let _,params = HExtlib.split_nth lno s' in
aux (k, e, List.nth pl (j-1), params@s)
| _ -> config, true)
in
let relevance = E.get_relevance r1 in
let relevance = match r1 with
| Ref.Ref (_,Ref.Con (_,_,lno)) ->
- let _,relevance = HExtlib.split_nth "NR 2" lno relevance in
+ let _,relevance = HExtlib.split_nth lno relevance in
HExtlib.mk_list false lno @ relevance
| _ -> relevance
in
| HExtlib.FailureAt fail ->
let relevance =
!get_relevance ~metasenv ~subst context hd1 tl1 in
- let _,relevance = HExtlib.split_nth "NR 3" fail relevance in
+ let _,relevance = HExtlib.split_nth fail relevance in
let b,relevance = (match relevance with
| [] -> assert false
| b::tl -> b,tl) in
if (not b) then
- let _,tl1 = HExtlib.split_nth "NR 4" (fail+1) tl1 in
- let _,tl2 = HExtlib.split_nth "NR 5" (fail+1) tl2 in
+ let _,tl1 = HExtlib.split_nth (fail+1) tl1 in
+ let _,tl2 = HExtlib.split_nth (fail+1) tl2 in
try
HExtlib.list_forall_default3
(fun t1 t2 b -> not b || aux true context t1 t2)