+ and case conclude =
+ let module P = Mpresentation in
+ let module Con = Content in
+ let proof_conclusion =
+ (match conclude.Con.conclude_conclusion with
+ None -> P.Mtext([],"No conclusion???")
+ | Some t -> term2pres t) in
+ let arg,args_for_cases =
+ (match conclude.Con.conclude_args with
+ Con.Aux(_)::Con.Aux(_)::Con.Term(_)::arg::tl ->
+ arg,tl
+ | _ -> assert false) in
+ let case_on =
+ let case_arg =
+ (match arg with
+ Con.Aux n ->
+ P.Mtext ([],"an aux???")
+ | Con.Premise prem ->
+ (match prem.Con.premise_binder with
+ None -> P.Mtext ([],"the previous result")
+ | Some n -> P.Mi([],n))
+ | Con.Lemma lemma -> P.Mi([],lemma.Con.lemma_name)
+ | Con.Term t ->
+ term2pres t
+ | Con.ArgProof p ->
+ P.Mtext ([],"a proof???")
+ | Con.ArgMethod s ->
+ P.Mtext ([],"a method???")) in
+ (make_concl "we proceede by cases on" case_arg) in
+ let to_prove =
+ (make_concl "to prove" proof_conclusion) in
+ P.Mtable
+ ([None,"align","baseline 1"; None,"equalrows","false";
+ None,"columnalign","left"],
+ P.Mtr ([],[P.Mtd ([],case_on)])::
+ P.Mtr ([],[P.Mtd ([],to_prove)])::
+ (make_cases args_for_cases))
+