From c9ea9ae384f7400e20f18049536299fd8521a8d4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 31 Jul 2003 15:41:05 +0000 Subject: [PATCH] Closed induction cases are now pointers to the acontext/conclusion ==> they are now perforated correctly. --- helm/ocaml/cic_transformations/content2pres.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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"], -- 2.39.2