- List.fold_right
- (fun (n, t) i -> "?" ^ (string_of_int n) ^ ": " ^ pp t [] ^ "\n" ^ i)
- conjectures "" ^
- "\n" ^ pp value [] ^ " : " ^ pp ty []
+ let separate s = if s = "" then "" else s ^ " ; " in
+ List.fold_right
+ (fun (n, context, t) i ->
+ let conjectures',name_context =
+ List.fold_right
+ (fun context_entry (i,name_context) ->
+ (match context_entry with
+ Some (n,C.Decl at) ->
+ (separate i) ^
+ string_of_name n ^ ":" ^ pp at name_context ^ " ",
+ (Some n)::name_context
+ | Some (n,C.Def at) ->
+ (separate i) ^
+ string_of_name n ^ ":= " ^ pp at name_context ^ " ",
+ (Some n)::name_context
+ | None ->
+ (separate i) ^ "_ :? _ ", None::name_context)
+ ) context ("",[])
+ in
+ conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
+ pp t name_context ^ "\n" ^ i
+ ) conjectures "" ^
+ "\n" ^ pp value [] ^ " : " ^ pp ty []