let classes, conclusion = Cl.classify c (H.get_type "opt_appl 3" c t) in
let csno, vsno = List.length classes, List.length vs in
if csno < vsno then
- let vvs, vs = HEL.split_nth "PO 1" csno vs in
+ let vvs, vs = HEL.split_nth csno vs in
let x = C.Appl (define c (C.Appl (t :: vvs)) :: vs) in
opt_proof g (info st "Optimizer: anticipate 2") true c x
else match conclusion, List.rev vs with
let eliminator = H.get_default_eliminator c uri tyno outty in
let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in
let ps, sort_disp = H.get_ind_parameters c arg in
- let lps, rps = HEL.split_nth "PO 2" lpsno ps in
+ let lps, rps = HEL.split_nth lpsno ps in
let rpsno = List.length rps in
if rpsno = 0 && sort_disp = 0 then
(* FG: the transformation is not possible, we fall back into the plain case *)