+ let acontext_id =
+ match p.Con.proof_apply_context with
+ [] -> p.Con.proof_conclude.Con.conclude_id
+ | {Con.proof_id = id}::_ -> id
+ in
+ B.Action([None,"type","toggle"],
+ [B.indent
+ (B.Text
+ ([None,"color","red" ;
+ Some "helm", "xref", acontext_id],"Proof")) ;
+ acontext2pres p.Con.proof_apply_context body true]) in
+ B.V ([], pattern::asubconcl::induction_hypothesis@[presacontext])
+ | _ -> 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 -> B.Text([],"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 -> [B.Text([],"Contradiction, hence")]
+ | Some n ->
+ [B.Object ([],P.Mi([],n)); B.skip;B.Text([],"is contradictory, hence")])
+ | Con.Lemma lemma ->
+ [B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip; B.Text([],"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 -> B.Text([],"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 -> [(B.b_kw "by"); B.b_space; B.Object([], P.Mi([],n))])
+ | Con.Lemma lemma ->
+ [(B.b_kw "by");B.skip; B.Object([], 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 =
+ B.H ([],
+ [B.Text([],"(");
+ B.Object ([], P.Mi([],get_name hyp1));
+ B.Text([],")");
+ B.skip;
+ term2pres hyp1.Con.dec_type]) in
+ let preshyp2 =
+ B.H ([],
+ [B.Text([],"(");
+ B.Object ([], P.Mi([],get_name hyp2));
+ B.Text([],")");
+ B.skip;
+ 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
+ B.V
+ ([],
+ [B.H ([],arg@[B.skip; B.Text([],"we have")]);
+ preshyp1;
+ B.Text([],"and");
+ preshyp2;
+ 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 -> B.Text([],"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 =
+ B.H ([],
+ [(B.b_kw "let");
+ B.skip;
+ B.Object ([], P.Mi([],get_name decl));
+ B.Text([],":"); term2pres decl.Con.dec_type]) in
+ let suchthat =
+ B.H ([],
+ [(B.b_kw "such that");
+ B.skip;
+ B.Text([],"(");
+ B.Object ([], P.Mi([],get_name hyp));
+ B.Text([],")");
+ B.skip;
+ 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
+ B.V
+ ([],
+ [presdecl;
+ suchthat;
+ presacontext]);
+ | _ -> assert false in