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