aux s ;
aux t
>]
+ | C.ALetIn (id,ann,_,s,t) ->
+ [< (match !ann with
+ None -> [<>]
+ | Some ann ->
+ (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
+ ) ;
+ aux s ;
+ aux t
+ >]
| C.AAppl (id,ann,li) ->
[< (match !ann with
None -> [<>]
) ;
print_term ty
>]
- | C.AVariable (xid, ann, _, ty) ->
+ | C.AVariable (xid, ann, _, bo, ty) ->
[< (match !ann with
None -> [<>]
| Some ann ->
X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
) ;
+ (match bo with
+ None -> [<>]
+ | Some bo -> print_term bo
+ ) ;
print_term ty
>]
| C.ACurrentProof (xid, ann, _, conjs, bo, ty) ->