| None ->
prerr_endline "NO NAME!!"; assert false)
| `Proof p ->
- (match p.Con.proof_name with
- Some "w" -> prerr_endline ("processing w");
- | _ -> ());
proof2pres p
| `Definition d ->
(match d.Con.def_name with
let module P = Mpresentation in
let tconclude_body =
match conclude.Con.conclude_conclusion with
- Some t when not omit_conclusion ->
+ Some t when
+ not omit_conclusion or
+ (* CSC: I ignore the omit_conclusion flag in this case. *)
+ (* CSC: Is this the correct behaviour? In the stylesheets *)
+ (* CSC: we simply generated nothing (i.e. the output type *)
+ (* CSC: of the function should become an option. *)
+ conclude.Con.conclude_method = "BU_Conversion" ->
let concl = (term2pres t) in
if conclude.Con.conclude_method = "BU_Conversion" then
make_concl "that is equivalent to" concl