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

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index cfa061bfb..0fbd5e458 100644
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -236,7 +236,8 @@ and proof2pres term2pres p =
             | Some ac ->
                P.Maction
                  ([None,"actiontype","toggle" ; None,"selection","1"],
-                  [(make_concl "proof of" ac); body])
+                  [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id]
+                     "proof of" ac); body])
           in
           P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
               None,"columnalign","left"],
@@ -303,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
@@ -341,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
@@ -611,8 +615,16 @@ and proof2pres term2pres p =
                acontext2pres_old p.Con.proof_apply_context true in *)
           let body = conclude2pres p.Con.proof_conclude true false in
           let presacontext = 
+           let acontext_id =
+            match p.Con.proof_apply_context with
+               [] -> p.Con.proof_conclude.Con.conclude_id
+             | {Con.proof_id = id}::_ -> id
+           in
             P.Maction([None,"actiontype","toggle" ; None,"selection","1"],
-              [P.indented (P.Mtext([None,"mathcolor","Red"],"Proof"));
+              [P.indented
+               (P.Mtext
+                 ([None,"mathcolor","Red" ;
+                   Some "helm", "xref", acontext_id],"Proof")) ;
                acontext2pres p.Con.proof_apply_context body true]) in
           P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
              None,"columnalign","left"],
@@ -849,7 +861,7 @@ let content2pres term2pres (id,params,metasenv,obj) =
                                            | Some n -> n) ;
                                         P.Mo [] ":=" ;
                                         proof2pres term2pres p]
-                               ) context @
+                               ) (List.rev context) @
                              [ P.Mo [] "|-" ] @
                              [ P.Mi [] (string_of_int n) ;
                                P.Mo [] ":" ;