(make_concl "we proved 1" conclusion))])]);
| _ -> assert false)
*)
+ else if (conclude.Con.conclude_method = "Case") then
+ case conclude
else if (conclude.Con.conclude_method = "ByInduction") then
byinduction conclude
else if (conclude.Con.conclude_method = "Exists") then
| Con.ArgMethod s ->
P.Mtext ([],"method")
+ 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))
+
and byinduction conclude =
let module P = Mpresentation in
let module Con = Content in
(Cexpr2pres.cexpr2pres_charcount
(Content_expressions.acic2cexpr ids_to_inner_sorts p)))
;;
+