X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=0fbd5e458e777b25270c849f9dad6edc5365067b;hb=4faf0e37e7019de16dd6862bb34d84f799a2a230;hp=a57ec0396731758266625b10a726370e820b6197;hpb=b993b6f15936219a54b2c057fc75ec1b8dde243a;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index a57ec0396..0fbd5e458 100644
--- 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