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"],
| Some n -> n) ;
P.Mo [] ":=" ;
proof2pres term2pres p]
- ) context @
+ ) (List.rev context) @
[ P.Mo [] "|-" ] @
[ P.Mi [] (string_of_int n) ;
P.Mo [] ":" ;