+ | _ -> assert false
+
+ and falseind 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 case_arg =
+ (match conclude.Con.conclude_args with
+ [Con.Aux(n);_;case_arg] -> case_arg
+ | _ -> assert false;
+ (*
+ List.map (ContentPp.parg 0) conclude.Con.conclude_args;
+ assert false *)) in
+ let arg =
+ (match case_arg with
+ Con.Aux n -> assert false
+ | Con.Premise prem ->
+ (match prem.Con.premise_binder with
+ None -> [P.Mtext([],"Contradiction, hence")]
+ | Some n ->
+ [P.Mi([],n);P.smallskip;P.Mtext([],"is contradictory, hence")])
+ | Con.Lemma lemma ->
+ [P.Mi([],lemma.Con.lemma_name);P.smallskip;P.Mtext([],"is contradictory, hence")]
+ | _ -> assert false) in
+ (* let body = proof2pres {proof with Con.proof_context = tl} in *)
+ make_row arg proof_conclusion
+
+ and andind 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 proof,case_arg =
+ (match conclude.Con.conclude_args with
+ [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg
+ | _ -> assert false;
+ (*
+ List.map (ContentPp.parg 0) conclude.Con.conclude_args;
+ assert false *)) in
+ let arg =
+ (match case_arg with
+ Con.Aux n -> assert false
+ | Con.Premise prem ->
+ (match prem.Con.premise_binder with
+ None -> []
+ | Some n -> [P.Mtext([],"by");P.smallskip;P.Mi([],n)])
+ | Con.Lemma lemma ->
+ [P.Mtext([],"by");P.smallskip;P.Mi([],lemma.Con.lemma_name)]
+ | _ -> assert false) in
+ match proof.Con.proof_context with
+ `Hypothesis hyp1::`Hypothesis hyp2::tl ->
+ let get_name hyp =
+ (match hyp.Con.dec_name with
+ None -> "_"
+ | Some s -> s) in
+ let preshyp1 =
+ P.Mrow ([],
+ [P.Mtext([],"(");
+ P.Mi([],get_name hyp1);
+ P.Mtext([],")");
+ P.smallskip;
+ term2pres hyp1.Con.dec_type]) in
+ let preshyp2 =
+ P.Mrow ([],
+ [P.Mtext([],"(");
+ P.Mi([],get_name hyp2);
+ P.Mtext([],")");
+ P.smallskip;
+ term2pres hyp2.Con.dec_type]) in
+ (* let body = proof2pres {proof with Con.proof_context = tl} in *)
+ let body = conclude2pres proof.Con.proof_conclude false true in
+ let presacontext =
+ acontext2pres proof.Con.proof_apply_context body false in
+ P.Mtable
+ ([None,"align","baseline 1"; None,"equalrows","false";
+ None,"columnalign","left"],
+ [P.Mtr ([],[P.Mtd ([],
+ P.Mrow([],arg@[P.smallskip;P.Mtext([],"we have")]))]);
+ P.Mtr ([],[P.Mtd ([],preshyp1)]);
+ P.Mtr ([],[P.Mtd ([],P.Mtext([],"and"))]);
+ P.Mtr ([],[P.Mtd ([],preshyp2)]);
+ P.Mtr ([],[P.Mtd ([],presacontext)])]);
+ | _ -> assert false
+
+ and exists 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 proof =
+ (match conclude.Con.conclude_args with
+ [Con.Aux(n);_;Con.ArgProof proof;_] -> proof
+ | _ -> assert false;
+ (*
+ List.map (ContentPp.parg 0) conclude.Con.conclude_args;
+ assert false *)) in
+ match proof.Con.proof_context with
+ `Declaration decl::`Hypothesis hyp::tl
+ | `Hypothesis decl::`Hypothesis hyp::tl ->
+ let get_name decl =
+ (match decl.Con.dec_name with
+ None -> "_"
+ | Some s -> s) in
+ let presdecl =
+ P.Mrow ([],
+ [P.Mtext([None,"mathcolor","Red"],"let");
+ P.smallskip;
+ P.Mi([],get_name decl);
+ P.Mtext([],":"); term2pres decl.Con.dec_type]) in
+ let suchthat =
+ P.Mrow ([],
+ [P.Mtext([None,"mathcolor","Red"],"such that");
+ P.smallskip;
+ P.Mtext([],"(");
+ P.Mi([],get_name hyp);
+ P.Mtext([],")");
+ P.smallskip;
+ term2pres hyp.Con.dec_type]) in
+ (* let body = proof2pres {proof with Con.proof_context = tl} in *)
+ let body = conclude2pres proof.Con.proof_conclude false true in
+ let presacontext =
+ acontext2pres proof.Con.proof_apply_context body false in
+ P.Mtable
+ ([None,"align","baseline 1"; None,"equalrows","false";
+ None,"columnalign","left"],
+ [P.Mtr ([],[P.Mtd ([],presdecl)]);
+ P.Mtr ([],[P.Mtd ([],suchthat)]);
+ P.Mtr ([],[P.Mtd ([],presacontext)])]);
+ | _ -> assert false in