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"))
let ugraph = CicUniv.oblivion_ugraph in
match obj with
Cic.Constant (name,Some bo,ty,args,attrs) ->
+prerr_endline ("PRIMA: " ^ CicPp.ppobj obj);
(* CSC: ugly code. Here I need to retrieve in advance the loc of bo
since type_of_aux' destroys localization information (which are
preserved by type_of_aux *)