From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 31 Jul 2003 15:41:05 +0000 (+0000)
Subject: Closed induction cases are now pointers to the acontext/conclusion ==>
X-Git-Tag: LucaOK~3
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c9ea9ae384f7400e20f18049536299fd8521a8d4;p=helm.git

Closed induction cases are now pointers to the acontext/conclusion ==>
they are now perforated correctly.
---

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 508d77fa0..e8699b8b4 100644
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -612,11 +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" ;
-                   Some "helm", "xref", p.Con.proof_id],"Proof")) ;
+                   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"],