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)
add_target_term ty
| C.ACurrentProof (id,_,cl,bo,ty) ->
set_target id (C.Object annobj) ;
- List.iter (function (_,context, t) ->
+ List.iter (function (cid,_,context, t) as annconj ->
+ set_target cid (C.Conjecture annconj) ;
List.iter
- (function
- Some (_,C.ADecl at) -> add_target_term at
- | Some (_,C.ADef at) -> add_target_term at
- | None -> ()
- ) context;
+ (function ((hid,h) as annhyp) ->
+ set_target hid (C.Hypothesis annhyp) ;
+ match h with
+ 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