-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_pair s ss u = function
+ | None ->
+ let name = X.rev_map_concat X.id "." "type" ss in
+ let och = open_out_tex name in
+ O.out_text och (proc_item "axiom" s u);
+ close_out och
+ | Some t ->
+ let text_u, text_t =
+ if A.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 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 t);
+ close_out och