- (separate i) ^
- ppname n ^ ":" ^
- pp ~metasenv:conjectures at name_context ^ " ",
- (Some n)::name_context
- | Some (n,C.Def (at,None)) ->
- (separate i) ^
- ppname n ^ ":= " ^ pp ~metasenv:conjectures
- at name_context ^ " ",
- (Some n)::name_context
- | None ->
- (separate i) ^ "_ :? _ ", None::name_context
- | _ -> assert false)
+ (separate i) ^
+ ppname n ^ ":" ^
+ pp ~metasenv:conjectures at name_context ^ " ",
+ (Some n)::name_context
+ | Some (n,C.Def (at,aty)) ->
+ (separate i) ^
+ ppname n ^ ": " ^
+ pp ~metasenv:conjectures aty name_context ^
+ ":= " ^ pp ~metasenv:conjectures
+ at name_context ^ " ",
+ (Some n)::name_context
+ | None ->
+ (separate i) ^ "_ :? _ ", None::name_context)