- P.Maction([None,"actiontype","toggle" ;
- None,"selection","1"],
- [(make_concl "proof of" ac);
- body]) in
+ match concl with
+ None -> body
+(*
+ P.Maction
+ ([None,"actiontype","toggle" ; None,"selection","1"],
+ [P.Mtext [] "proof" ; body])
+*)
+ | Some ac ->
+ P.Maction
+ ([None,"actiontype","toggle" ; None,"selection","1"],
+ [(make_concl "proof of" ac); body])
+ in