X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=e8699b8b4445d24f04d585b6c7c21dbbcbb18ada;hb=962cc970cd9a2161f69b70aa01b6ee9e289d9778;hp=9a5ad74fd9f6d954eb1202f04ac3b7f75be6fc29;hpb=ef7c0b39d038ea5e64595f14b766683d7572833a;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 9a5ad74fd..e8699b8b4 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"],
@@ -611,8 +612,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"],
@@ -810,13 +819,13 @@ let content2pres term2pres (id,params,metasenv,obj) =
                            (P.Mrow [Some "helm", "xref", id]
                              (List.map
                                (function
-                                   (_,None) ->
+                                   None ->
                                      P.Mrow []
                                       [ P.Mi [] "_" ;
                                         P.Mo [] ":?" ;
                                         P.Mi [] "_"]
-                                 | (_,Some (`Declaration d))
-                                 | (_,Some (`Hypothesis d)) ->
+                                 | Some (`Declaration d)
+                                 | Some (`Hypothesis d) ->
                                     let
                                      { K.dec_name = dec_name ;
                                        K.dec_type = ty } = d
@@ -828,7 +837,7 @@ let content2pres term2pres (id,params,metasenv,obj) =
                                             | Some n -> n) ;
                                          P.Mo [] ":" ;
                                          term2pres ty]
-                                 | (_,Some (`Definition d)) ->
+                                 | Some (`Definition d) ->
                                     let
                                      { K.def_name = def_name ;
                                        K.def_term = bo } = d
@@ -840,7 +849,7 @@ let content2pres term2pres (id,params,metasenv,obj) =
                                             | Some n -> n) ;
                                          P.Mo [] ":=" ;
                                          term2pres bo]
-                                 | (_,Some (`Proof p)) ->
+                                 | Some (`Proof p) ->
                                     let proof_name = p.K.proof_name in
                                      P.Mrow []
                                       [ P.Mi []
@@ -849,7 +858,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 [] ":" ;