+let get_ids_to_targets annobj =
+ let module C = Cic in
+ let ids_to_targets = Hashtbl.create 503 in
+ let set_target id target =
+ try
+ ignore (Hashtbl.find ids_to_targets id) ;
+ raise (MoreThanOneTargetFor id)
+ with
+ Not_found -> Hashtbl.add ids_to_targets id target
+ in
+ let rec add_target_term t =
+ match t with
+ C.ARel (id,_,_)
+ | C.AVar (id,_)
+ | C.AMeta (id,_)
+ | C.ASort (id,_)
+ | C.AImplicit id ->
+ set_target id (C.Term t)
+ | C.ACast (id,va,ty) ->
+ set_target id (C.Term t) ;
+ add_target_term va ;
+ add_target_term ty
+ | C.AProd (id,_,so,ta)
+ | C.ALambda (id,_,so,ta)
+ | C.ALetIn (id,_,so,ta) ->
+ set_target id (C.Term t) ;
+ add_target_term so ;
+ add_target_term ta
+ | C.AAppl (id,l) ->
+ set_target id (C.Term t) ;
+ List.iter add_target_term l
+ | C.AConst (id,_,_)
+ | C.AAbst (id,_)
+ | C.AMutInd (id,_,_,_)
+ | C.AMutConstruct (id,_,_,_,_) ->
+ set_target id (C.Term t)
+ | C.AMutCase (id,_,_,_,ot,it,pl) ->
+ set_target id (C.Term t) ;
+ List.iter add_target_term (ot::it::pl)
+ | C.AFix (id,_,ifl) ->
+ set_target id (C.Term t) ;
+ List.iter
+ (function (_,_,ty,bo) ->
+ add_target_term ty ;
+ add_target_term bo
+ ) ifl
+ | C.ACoFix (id,_,cfl) ->
+ set_target id (C.Term t) ;
+ List.iter
+ (function (_,ty,bo) ->
+ add_target_term ty ;
+ add_target_term bo
+ ) cfl
+ in
+ let add_target_obj annobj =
+ match annobj with
+ C.ADefinition (id,_,bo,ty,_) ->
+ set_target id (C.Object annobj) ;
+ add_target_term bo ;
+ add_target_term ty
+ | C.AAxiom (id,_,ty,_) ->
+ set_target id (C.Object annobj) ;
+ add_target_term ty
+ | C.AVariable (id,_,None,ty) ->
+ set_target id (C.Object annobj) ;
+ add_target_term ty
+ | C.AVariable (id,_,Some bo,ty) ->
+ set_target id (C.Object annobj) ;
+ add_target_term bo ;
+ add_target_term ty
+ | C.ACurrentProof (id,_,cl,bo,ty) ->
+ set_target id (C.Object annobj) ;
+ List.iter (function (_,t) -> add_target_term t) cl ;
+ add_target_term bo ;
+ add_target_term ty
+ | C.AInductiveDefinition (id,itl,_,_) ->
+ set_target id (C.Object annobj) ;
+ List.iter
+ (function (_,_,arity,cl) ->
+ add_target_term arity ;
+ List.iter (function (_,ty,_) -> add_target_term ty) cl
+ ) itl
+ in
+ add_target_obj annobj ;
+ ids_to_targets