- 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))
+ let scontext,context = ppcontext' ~metasenv ~sep:"; " subst c in
+ sprintf "%s |- ?%d : %s := %s" scontext idx
+(ppterm_in_context ~metasenv [] ty context)
+ (ppterm_in_context ~metasenv subst t context))