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

[helm.git] / helm / ocaml / cic_transformations / content2pres.ml

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