let vty = match vty with
| C.Appl (C.MutInd (fu, fm, _) as hd :: args)
when UM.eq fu u && fm = m && List.length args = psno ->
- let largs, _ = X.split_nth "D 1" lpsno args in
+ let largs, _ = X.split_nth lpsno args in
C.Appl (hd :: largs @ Ut.mk_rels rpsno 0)
| _ ->
assert false