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) ->
+ 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) ->
+ string_of_name n ^ ":" ^ pp at name_context ^ " ",
+ (Some n)::name_context
+ | Some (n,C.Def (at,None)) ->
(separate i) ^
- string_of_name n ^ ":= " ^ pp at name_context ^ " ",
- (Some n)::name_context
+ string_of_name n ^ ":= " ^ pp at name_context ^ " ",
+ (Some n)::name_context
| None ->
- (separate i) ^ "_ :? _ ", None::name_context)
- ) context ("",[])
+ (separate i) ^ "_ :? _ ", None::name_context
+ | _ -> assert false)
+ ) context ("",[])
in
conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
pp t name_context ^ "\n" ^ i