+let string_of_atomic = function
+ | C.ARel (_, _, _, s) -> s
+ | C.AVar (_, uri, _) -> H.name_of_uri uri None None
+ | C.AConst (_, uri, _) -> H.name_of_uri uri None None
+ | C.AMutInd (_, uri, i, _) -> H.name_of_uri uri (Some i) None
+ | C.AMutConstruct (_, uri, i, j, _) -> H.name_of_uri uri (Some i) (Some j)
+ | _ -> ""
+
+let get_sub_names head l =
+ let s = string_of_atomic head in
+ if s = "" then [] else
+ let map (names, i) _ =
+ let name = Printf.sprintf "%s_%u" s i in name :: names, succ i
+ in
+ let names, _ = List.fold_left map ([], 1) l in
+ List.rev names
+