From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 31 Jul 2003 14:44:25 +0000 (+0000)
Subject: "proof of X" closed mactions were not selectable
X-Git-Tag: LucaOK~5
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fdb0f0fada932df83ab4df53d4ea463a8794d513;p=helm.git

"proof of X" closed mactions were not selectable
---

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 69b0966f1..508d77fa0 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"],