- (fun (idx, (c, t,_)) ->
- let context,name_context = ppcontext' ~sep:"; " subst c in
- sprintf "%s |- ?%d:= %s" context idx
- (ppterm_in_name_context subst t name_context))
+ (fun (idx, (c, t,ty)) ->
+ let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in
+ sprintf "%s |- ?%d : %s := %s" context idx
+(ppterm_in_name_context ~metasenv [] ty name_context)
+ (ppterm_in_name_context ~metasenv subst t name_context))