| 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"],
| None ->
prerr_endline "NO NAME!!"; assert false)
| `Proof p ->
- (match p.Con.proof_name with
- Some "w" -> prerr_endline ("processing w");
- | _ -> ());
proof2pres p
| `Definition d ->
(match d.Con.def_name with
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"],