BU_Conversion + omit-conclusion is a mess. I have partially fixed the

problem by ignoring the omit-conclusion flag.

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index a57ec0396731758266625b10a726370e820b6197..0fbd5e458e777b25270c849f9dad6edc5365067b 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -339,7 +339,13 @@ and proof2pres term2pres p =
     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