+(* ids_to_terms should not be passed here, is just for debugging *)
+let find_root_id annobj id ids_to_father_ids ids_to_terms =
+ let find_parent id ids =
+ let rec aux id =
+(* (prerr_endline (sprintf "id %s = %s" id
+ (try
+ CicPp.ppterm (Hashtbl.find ids_to_terms id)
+ with Not_found -> "NONE"))); *)
+ if List.mem id ids then Some id
+ else
+ (match
+ (try Hashtbl.find ids_to_father_ids id with Not_found -> None)
+ with
+ | None -> None
+ | Some id' -> aux id')
+ in
+ aux id
+ in
+ let return_father id ids =
+ match find_parent id ids with
+ | None -> assert false
+ | Some parent_id -> parent_id
+ in
+ let mk_ids terms = List.map CicUtil.id_of_annterm terms in
+ match annobj with
+ | Cic.AConstant (_, _, _, Some bo, ty, _, _)
+ | Cic.AVariable (_, _, Some bo, ty, _, _)
+ | Cic.ACurrentProof (_, _, _, _, bo, ty, _, _) ->
+ return_father id (mk_ids [ty; bo])
+ | Cic.AConstant (_, _, _, None, ty, _, _)
+ | Cic.AVariable (_, _, None, ty, _, _) -> return_father id (mk_ids [ty])
+ | Cic.AInductiveDefinition _ ->
+ assert false (* TODO *)
+