From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 13 Apr 2006 14:23:30 +0000 (+0000)
Subject: partially fixed  boxes in rewite
X-Git-Tag: make_still_working~7410
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=780561e45e8de50dd0063a0e369458ba67479872;p=helm.git

partially fixed  boxes in rewite
---

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