List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]
>]
| C.AConst (id,_,_) -> print_ann i2a id
- | C.AAbst (id,_) -> raise NotImplemented
| C.AMutInd (id,_,_,_) -> print_ann i2a id
| C.AMutConstruct (id,_,_,_,_) -> print_ann i2a id
| C.AMutCase (id,_,_,_,ty,te,patterns) ->
| 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 -> [< >]