+let content2pres term2pres (id,params,metasenv,obj) =
+ let module Con = Cic2content in
+ let module P = Mpresentation in
+ match obj with
+ `Def (Con.Const,thesis,`Proof p) ->
+ P.Mtable
+ [None,"align","baseline 1";
+ None,"equalrows","false";
+ None,"columnalign","left";
+ None,"helm:xref","id"]
+ [(*P.Mtr []
+ [P.Mtd []
+ (P.Mrow []
+ [P.Mtext [] ("UNFINISHED PROOF" ^ id ^"(" ^ params ^ ")")])] ;
+*)
+ P.Mtr []
+ [P.Mtd []
+ (P.Mrow []
+ [P.Mtext [] "THESIS:"])] ;
+ P.Mtr []
+ [P.Mtd []
+ (P.Mrow []
+ [P.Mphantom []
+ (P.Mtext [] "__") ;
+ term2pres thesis])] ;
+ P.Mtr []
+ [P.Mtd []
+ (P.Mrow []
+ [proof2pres term2pres p])]]
+ | _ -> raise ToDo
+;;