match CicReduction.whd context tty with
Cic.MutInd (_,_,ens) -> ens,[]
| Cic.Appl (Cic.MutInd (_,_,ens)::args) ->
- ens,fst (HExtlib.split_nth "ON 1" leftno args)
+ ens,fst (HExtlib.split_nth leftno args)
| _ -> assert false
in
let rec aux n irl context outsort =