let get_l_r_p n = function
| Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
| Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
- HExtlib.split_nth "R 1" n args
+ HExtlib.split_nth n args
| _ -> assert false
in
let _, _, ty, cl = List.nth tl tyno in
(CR.head_beta_reduce ~delta:false
(Cic.Appl [outty;k])))),k
| Cic.Appl (Cic.MutInd _::pl) ->
- let left_p,right_p = HExtlib.split_nth "R 2" leftno pl in
+ let left_p,right_p = HExtlib.split_nth leftno pl in
let has_rights = right_p <> [] in
let k =
let k = Cic.MutConstruct (uri,tyno,i,[]) in
CicUniv.oblivion_ugraph
with
| Cic.Appl (Cic.MutInd _::args),_ ->
- snd (HExtlib.split_nth "R 3" leftno args)
+ snd (HExtlib.split_nth leftno args)
| _ -> assert false
with CicTypeChecker.TypeCheckerFailure _-> assert false
in
with
| (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
| Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
- snd (HExtlib.split_nth "R 4" leftno args), mty
+ snd (HExtlib.split_nth leftno args), mty
| _ -> assert false
with CicTypeChecker.TypeCheckerFailure _ ->
raise (AssertFailure(lazy "already ill-typed matched term"))