X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=1616c21c8273d0bf15b9fc4ba39948a3e328e8c4;hb=60951dd6218b8436830723dc10d4aed7b6894855;hp=cd7bac62544b101ad2be9b0d61e30d21e559713b;hpb=6baf07f7ebd9b40e642467f01a66920d9fb1448a;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index cd7bac625..1616c21c8 100644
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -220,15 +220,19 @@ and proof2pres term2pres p =
       match p.Con.proof_name with
         None -> body
       | Some name ->
-          let ac = 
-        (match concl with
-               None -> P.Mtext([],"NO PROOF!!!")
-             | Some c -> c) in 
           let action = 
-            P.Maction([None,"actiontype","toggle" ;
-                       None,"selection","1"],
-              [(make_concl "proof of" ac);
-                body]) in
+           match concl with
+              None -> body
+(*
+               P.Maction
+                 ([None,"actiontype","toggle" ; None,"selection","1"],
+                  [P.Mtext [] "proof" ; body])
+*)
+            | Some ac ->
+               P.Maction
+                 ([None,"actiontype","toggle" ; None,"selection","1"],
+                  [(make_concl "proof of" ac); body])
+          in
           P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
               None,"columnalign","left"],
             [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]);
@@ -371,16 +375,19 @@ and proof2pres term2pres p =
     else if conclude.Con.conclude_method = "BU_Conversion" then
       assert false
     else if conclude.Con.conclude_method = "Exact" then
-      let conclusion = 
-        (match conclude.Con.conclude_conclusion with 
-           None -> P.Mtext([],"NO Conclusion!!!")
-         | Some c -> term2pres c) in
       let arg = 
         (match conclude.Con.conclude_args with 
            [Con.Term t] -> term2pres t
          | _ -> assert false) in
-      make_row 
-        [arg;P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] conclusion
+      (match conclude.Con.conclude_conclusion with 
+         None ->
+          P.Mrow []
+           [P.Mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg]
+       | Some c -> let conclusion = term2pres c in
+          make_row 
+            [arg; P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")]
+            conclusion
+       )
     else if conclude.Con.conclude_method = "Intros+LetTac" then
       (match conclude.Con.conclude_args with
          [Con.ArgProof p] -> proof2pres p
@@ -693,7 +700,7 @@ let content2pres term2pres (id,params,metasenv,obj) =
                        (id,n,context,ty) ->
                          P.Mtr []
                           [P.Mtd []
-                           (P.Mrow []
+                           (P.Mrow [Some "helm", "xref", id]
                              (List.map
                                (function
                                    (_,None) ->