From: Claudio Sacerdoti Coen Date: Tue, 23 Sep 2003 15:56:42 +0000 (+0000) Subject: BU_Conversion + omit-conclusion is a mess. I have partially fixed the X-Git-Tag: V_0_4_3_4~16 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=faf362d25c28585add8c951300da0a54993d0d67;p=helm.git 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 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