+let ppcontext ?(sep = "\n") context =
+ let separate s = if s = "" then "" else s ^ sep in
+ fst (List.fold_right
+ (fun context_entry (i,name_context) ->
+ match context_entry with
+ Some (n,Cic.Decl t) ->
+ Printf.sprintf "%s%s : %s" (separate i) (ppname n)
+ (pp t name_context), (Some n)::name_context
+ | Some (n,Cic.Def (bo,ty)) ->
+ Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
+ (match ty with
+ None -> "_"
+ | Some ty -> pp ty name_context)
+ (pp bo name_context), (Some n)::name_context
+ | None ->
+ Printf.sprintf "%s_ :? _" (separate i), None::name_context
+ ) context ("",[]))
+