let patterns,outtype =
match fst (CicEnvironment.get_obj CU.oblivion_ugraph turi) with
| C.InductiveDefinition (ind_type_list,_,paramsno,_)->
- let left_params, right_params = HExtlib.split_nth "DT 1" paramsno params in
+ let left_params, right_params = HExtlib.split_nth paramsno params in
let _,_,_,constructor_list = List.nth ind_type_list typeno in
let i_constr_id,_ = List.nth constructor_list (consno - 1) in
let patterns =
match S.lift 1 tty with
| C.MutInd _ as tty' -> tty'
| C.Appl l ->
- let keep,abstract = HExtlib.split_nth "DT 2" (paramsno +1) l in
+ let keep,abstract = HExtlib.split_nth (paramsno +1) l in
let keep = List.map (S.lift paramsno) keep in
C.Appl (keep@mk_rels (List.length abstract))
| _ -> assert false