From 780561e45e8de50dd0063a0e369458ba67479872 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 13 Apr 2006 14:23:30 +0000 Subject: [PATCH] partially fixed boxes in rewite --- .../components/content_pres/content2pres.ml | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index abac7cb5d..543ea0ac8 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -130,8 +130,10 @@ let rec justification term2pres p = make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in B.H([], (B.b_kw "by")::B.b_space:: - B.Text([],"(")::pres_args@[B.Text([],")")]) - else proof2pres term2pres p + B.Text([],"(")::pres_args@[B.Text([],")")]), None + else + (B.b_kw "by"), + Some (B.b_toggle [B.b_kw "proof";proof2pres term2pres p]) and proof2pres term2pres p = let rec proof2pres p = @@ -358,7 +360,7 @@ and proof2pres term2pres p = else if (conclude.Con.conclude_method = "FalseInd") then falseind conclude else if (conclude.Con.conclude_method = "Rewrite") then - let justif = + let justif1, justif2 = (match (List.nth conclude.Con.conclude_args 6) with Con.ArgProof p -> justification term2pres p | _ -> assert false) in @@ -371,12 +373,13 @@ and proof2pres term2pres p = Con.Term t -> term2pres t | _ -> assert false) in B.V ([], - [B.H ([],[ + B.H ([],[ (B.b_kw "rewrite"); B.b_space; term1; B.b_space; (B.b_kw "with"); - B.b_space; term2; - B.indent justif])]) + B.b_space; term2; + B.b_space; justif1]) :: + match justif2 with None -> [] | Some j -> [B.indent j]) else if conclude.Con.conclude_method = "Apply" then let pres_args = make_args_for_apply term2pres conclude.Con.conclude_args in -- 2.39.2