C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
dummy
| C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
- let _, rargs = HExtlib.split_nth "TC 1" leftno tl in
+ let _, rargs = HExtlib.split_nth leftno tl in
if rargs = [] then dummy else Cic.Appl (dummy :: rargs)
| C.Cast (te,ty) -> subst_inductive_type_with_dummy te
| C.Prod (name,so,ta) ->
let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
(match o with
| Cic.InductiveDefinition (tl,_,paramsno,_) ->
- let left_args,_ = HExtlib.split_nth "TC 2" paramsno args in
+ let left_args,_ = HExtlib.split_nth paramsno args in
List.map (fun (name, isind, arity, cl) ->
let arity = CicSubstitution.subst_vars exp arity in
let arity = instantiate_parameters left_args arity in
("Too many args for constructor: " ^ String.concat " "
(List.map (fun x-> CicPp.ppterm x) args))))
in
- let left, args = HExtlib.split_nth "TC 3" paramsno tl in
+ let left, args = HExtlib.split_nth paramsno tl in
List.for_all (does_not_occur ~subst context n nn) left &&
analyse_instantiated_type rec_params args
| C.Appl ((C.MutCase (_,_,out,te,pl))::_)