- open_out (F.concat !G.out_dir (s ^ T.file_ext))
-
-let proc_pair s ss u xt =
- let name = X.rev_map_concat X.id "." "type" ss in
- let och = open_out_tex name in
- O.out_text och (proc_top_type s u);
- close_out och;
- match xt with
- | None -> ()
- | Some t ->
- let name = X.rev_map_concat X.id "." "body" ss in
- let och = open_out_tex name in
- let text = if A.not_prop1 [] u then proc_top_body else proc_top_proof in
- O.out_text och (text s t);
- close_out och
-
-let proc_fun ss (r, s, i, u, t) =
+ let fname = s ^ T.file_ext in
+ begin match !G.list_och with
+ | None -> ()
+ | Some och -> P.fprintf och "%s\n" fname
+ end;
+ open_out (F.concat !G.out_dir fname)
+
+let proc_pair s ss u = function
+ | None ->
+ let text_u =
+ if K.not_prop1 [] u then proc_item "assumption"
+ else proc_item "axiom"
+ in
+ let name = X.rev_map_concat X.id "." "type" ss in
+ let och = open_out_tex name in
+ O.out_text och (text_u s name u);
+ close_out och
+ | Some t ->
+ let text_u, text_t =
+ if K.not_prop1 [] u then proc_item "declaration", proc_item "definition"
+ else proc_item "proposition", proc_top_proof
+ in
+ let name = X.rev_map_concat X.id "." "type" ss in
+ let och = open_out_tex name in
+ O.out_text och (text_u s name u);
+ close_out och;
+ let name = X.rev_map_concat X.id "." "body" ss in
+ let och = open_out_tex name in
+ O.out_text och (text_t s name t);
+ close_out och
+
+let proc_fun ss (_r, s, _i, u, t) =