| C.ACurrentProof (xid, _, conjs, bo, ty) ->
[< print_ann i2a xid ;
List.fold_right
- (fun (_, context, t) i ->
- [< List.fold_right
- (fun context_entry i ->
- [<(match context_entry with
+ (fun (cid, _, context, t) i ->
+ [< print_ann i2a cid ;
+ List.fold_right
+ (fun (hid,context_entry) i ->
+ [<print_ann i2a hid ;
+ (match context_entry with
Some (_,C.ADecl at) -> print_term i2a at
| Some (_,C.ADef at) -> print_term i2a at
| None -> [< >]