1. folded maction are now selectable

[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 cfa061bfb2e442c93da5457d2fa7545ccf444edc..69b0966f10b205fb3845b86f08e1d9d2f0763a21 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -612,7 +612,10 @@ and proof2pres term2pres p =
           let body = conclude2pres p.Con.proof_conclude true false in
           let presacontext = 
             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", p.Con.proof_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 +852,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 [] ":" ;