From faf362d25c28585add8c951300da0a54993d0d67 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 23 Sep 2003 15:56:42 +0000 Subject: [PATCH] BU_Conversion + omit-conclusion is a mess. I have partially fixed the problem by ignoring the omit-conclusion flag. --- helm/ocaml/cic_transformations/content2pres.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) 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 -- 2.39.2