From 0ac6c9a8f9cb3206002178edcf2dfa761c7a94ef Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 30 Jun 2007 12:11:01 +0000 Subject: [PATCH] Nicer layout but possibly more bugged. We need continuations here to do a good job. --- .../components/content_pres/content2pres.ml | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index 018497404..5620b6847 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -283,7 +283,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = B.b_hv [] (make_concl "that is equivalent to" concl :: if is_top_down then [B.b_space ; B.b_kw "done"; - B.Text([],".")] else []) + B.Text([],".")] else [B.Text([],".")]) else if conclude.Con.conclude_method = "FalseInd" then (* false ind is in charge to add the conclusion *) falseind conclude @@ -351,8 +351,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = B.V ([], [make_concl "we need to prove" expected; - make_concl "or equivalently" synth; - B.Text([],"."); + B.H ([],[make_concl "or equivalently" synth; B.Text([],".")]); proof2pres true subproof false]) else if conclude.Con.conclude_method = "BU_Conversion" then assert false @@ -532,8 +531,8 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = | Con.ArgMethod s -> B.b_kw "a method???") in (make_concl "we proceed by induction on" arg) in let to_prove = - (make_concl "to prove" proof_conclusion) in - B.V ([], induction_on::to_prove:: B.Text([],".")::(make_cases args_for_cases)) + B.H ([], [make_concl "to prove" proof_conclusion ; B.Text([],".")]) in + B.V ([], induction_on::to_prove::(make_cases args_for_cases)) and make_cases l = List.map make_case l @@ -614,7 +613,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = p.Con.proof_apply_context body true (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") ]) in - B.V ([], pattern::induction_hypothesis@[asubconcl;B.Text([],".");presacontext]) + B.V ([], pattern::induction_hypothesis@[B.H ([],[asubconcl;B.Text([],".")]);presacontext]) | _ -> assert false and falseind conclude = @@ -869,7 +868,7 @@ let content2pres [Some "helm","xref","id"] ([ B.b_h [] (B.b_kw ("theorem " ^ name) :: params2pres params @ [B.b_kw ":"]); - B.indent (term2pres thesis) ; B.b_kw "." ] @ + B.H ([],[B.indent (term2pres thesis) ; B.b_kw "." ])] @ metasenv2pres term2pres metasenv @ [proof ; B.b_kw "qed."]) | `Def (_, ty, `Definition body) -> -- 2.39.2