exception MoreThanOneTargetFor of Cic.id;;
+(* creates a hashtable mapping each unique id to a node of the annotated
+object *)
let get_ids_to_targets annobj =
let module C = Cic in
let ids_to_targets = Hashtbl.create 503 in
match t with
C.ARel (id,_,_)
| C.AVar (id,_)
- | C.AMeta (id,_)
+ | C.AMeta (id,_,_)
| C.ASort (id,_)
| C.AImplicit id ->
set_target id (C.Term t)
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 ;
+ List.iter (function (_,context, t) ->
+ List.iter
+ (function
+ Some (_,C.ADecl at) -> add_target_term at
+ | Some (_,C.ADef at) -> add_target_term at
+ | None -> ()
+ ) context;
+ add_target_term t) cl ;
add_target_term bo ;
add_target_term ty
| C.AInductiveDefinition (id,itl,_,_) ->