in
let rec add_target_term t =
match t with
- C.ARel (id,_,_)
- | C.AVar (id,_)
+ C.ARel (id,_,_,_)
| C.AMeta (id,_,_)
| C.ASort (id,_)
- | C.AImplicit id ->
+ | C.AImplicit (id, _) ->
set_target id (C.Term t)
| C.ACast (id,va,ty) ->
set_target id (C.Term t) ;
| C.AAppl (id,l) ->
set_target id (C.Term t) ;
List.iter add_target_term l
- | C.AConst (id,_,_)
- | C.AMutInd (id,_,_,_)
- | C.AMutConstruct (id,_,_,_,_) ->
- set_target id (C.Term t)
- | C.AMutCase (id,_,_,_,ot,it,pl) ->
+ | C.AVar (id,_,exp_named_subst)
+ | C.AConst (id,_,exp_named_subst)
+ | C.AMutInd (id,_,_,exp_named_subst)
+ | C.AMutConstruct (id,_,_,_,exp_named_subst) ->
+ set_target id (C.Term t) ;
+ List.iter (function (_,t) -> add_target_term t) exp_named_subst
+ | 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) ->
+ (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) ->
+ (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,_) ->
+ C.AConstant (id,idbody,_,bo,ty,_) ->
set_target id (C.Object annobj) ;
+ (match idbody,bo with
+ Some idbody,Some bo ->
+ set_target idbody (C.ConstantBody annobj) ;
+ add_target_term bo
+ | None, None -> ()
+ | _,_ -> 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,_,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 ->
set_target cid (C.Conjecture annconj) ;
List.iter
| C.AInductiveDefinition (id,itl,_,_) ->
set_target id (C.Object annobj) ;
List.iter
- (function (_,_,arity,cl) ->
+ (function (_,_,_,arity,cl) ->
add_target_term arity ;
- List.iter (function (_,ty,_) -> add_target_term ty) cl
+ List.iter (function (_,ty) -> add_target_term ty) cl
) itl
in
add_target_obj annobj ;