X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcontent_pres%2Fcontent2pres.ml;h=7c0ad99c476072685ce7454832f03da6dccfcb50;hb=e3ed04fe2299bdb814ee077e60f1046a86156982;hp=abac7cb5deca46fd88f1acf4be241d8ca8b6b5fa;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/content_pres/content2pres.ml b/components/content_pres/content2pres.ml
index abac7cb5d..7c0ad99c4 100644
--- a/components/content_pres/content2pres.ml
+++ b/components/content_pres/content2pres.ml
@@ -112,7 +112,6 @@ let make_args_for_apply term2pres args =
       make_arg_for_apply true hd 
         (List.fold_right (make_arg_for_apply false) tl [])
   | _ -> assert false
-
 let get_name = function
   | Some s -> s
   | None -> "_"
@@ -130,8 +129,9 @@ 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 +358,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 +371,32 @@ 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; justif1])::
+	    match justif2 with None -> [] | Some j -> [B.indent j])
+    else if conclude.Con.conclude_method = "Eq_chain" then
+      let justification p =
+	let j1,j2 = justification term2pres p in
+	  j1 :: B.b_space :: (match j2 with Some j -> [j] | None -> [])
+      in
+      let rec aux args =
+	match args with
+	  | [] -> []
+	  | (Con.ArgProof p)::(Con.Term t)::tl -> 
+	      B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw "=";B.b_space;term2pres t;B.b_space]@justification p))::(aux tl)
+	  | _ -> assert false 
+      in
+      let hd = 
+	match List.hd conclude.Con.conclude_args with
+	  | Con.Term t -> t 
+	  | _ -> assert false 
+      in
+      B.HOV([],[term2pres hd; (* B.b_space; *)
+	      B.V ([],aux (List.tl conclude.Con.conclude_args))])
     else if conclude.Con.conclude_method = "Apply" then
       let pres_args = 
         make_args_for_apply term2pres conclude.Con.conclude_args in