+let get_checked_indtys = function
+ | NReference.Ref (_, uri, NReference.Ind n) ->
+ (match get_checked_obj uri with
+ | _,_,_,_, NCic.Inductive (inductive,leftno,tys,att) ->
+ inductive,leftno,tys,att,n
+ | _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false)
+ | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false
+;;
+