in
let add_target_obj annobj =
match annobj with
- C.AConstant (id,idbody,_,bo,ty,_) ->
+ C.AConstant (id,idbody,_,bo,ty,_,_) ->
set_target id (C.Object annobj) ;
(match idbody,bo with
Some idbody,Some bo ->
| _,_ -> assert false
) ;
add_target_term ty
- | C.AVariable (id,_,None,ty,_) ->
+ | C.AVariable (id,_,None,ty,_,_) ->
set_target id (C.Object annobj) ;
add_target_term ty
- | C.AVariable (id,_,Some bo,ty,_) ->
+ | C.AVariable (id,_,Some bo,ty,_,_) ->
set_target id (C.Object annobj) ;
add_target_term bo ;
add_target_term ty
- | C.ACurrentProof (id,idbody,_,cl,bo,ty,_) ->
+ | C.ACurrentProof (id,idbody,_,cl,bo,ty,_,_) ->
set_target id (C.Object annobj) ;
set_target idbody (C.ConstantBody annobj) ;
List.iter (function (cid,_,context, t) as annconj ->
add_target_term t) cl ;
add_target_term bo ;
add_target_term ty
- | C.AInductiveDefinition (id,itl,_,_) ->
+ | C.AInductiveDefinition (id,itl,_,_,_) ->
set_target id (C.Object annobj) ;
List.iter
(function (_,_,_,arity,cl) ->