X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=a8b0bc6a039e78425fe942ce6464770ddbabba1e;hb=b3ce13018a7e6230313124ee2428a91ec5109e51;hp=543ea0ac8436c8bc39bed6f31b74aeadcf587341;hpb=780561e45e8de50dd0063a0e369458ba67479872;p=helm.git

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 543ea0ac8..a8b0bc6a0 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -130,9 +130,8 @@ 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([],")")]), None
-  else 
-    (B.b_kw "by"),
+      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 =
@@ -211,44 +210,32 @@ and proof2pres term2pres p =
   and ce2pres = 
     function 
         `Declaration d -> 
-          (match d.Con.dec_name with
-              Some s ->
-                let ty = term2pres d.Con.dec_type in
-                B.H ([],
-                  [(B.b_kw "Assume");
-                   B.b_space;
-                   B.Object ([], P.Mi([],s));
-                   B.Text([],":");
-                   ty])
-            | None -> 
-                prerr_endline "NO NAME!!"; assert false)
+         let ty = term2pres d.Con.dec_type in
+         B.H ([],
+           [(B.b_kw "Assume");
+            B.b_space;
+            B.Object ([], P.Mi([],get_name d.Con.dec_name));
+            B.Text([],":");
+            ty])
       | `Hypothesis h ->
-          (match h.Con.dec_name with
-              Some s ->
-                let ty = term2pres h.Con.dec_type in
-                B.H ([],
-                  [(B.b_kw "Suppose");
-                   B.b_space;
-                   B.Text([],"(");
-                   B.Object ([], P.Mi ([],s));
-                   B.Text([],")");
-                   B.b_space;
-                   ty])
-            | None -> 
-                prerr_endline "NO NAME!!"; assert false) 
+          let ty = term2pres h.Con.dec_type in
+          B.H ([],
+            [(B.b_kw "Suppose");
+             B.b_space;
+             B.Text([],"(");
+             B.Object ([], P.Mi ([],get_name h.Con.dec_name));
+             B.Text([],")");
+             B.b_space;
+             ty])
       | `Proof p -> 
            proof2pres p 
       | `Definition d -> 
-           (match d.Con.def_name with
-              Some s ->
-                let term = term2pres d.Con.def_term in
-                B.H ([],
-                  [ B.b_kw "Let"; B.b_space;
-                    B.Object ([], P.Mi([],s));
-                    B.Text([]," = ");
-                    term])
-            | None -> 
-                prerr_endline "NO NAME!!"; assert false) 
+          let term = term2pres d.Con.def_term in
+          B.H ([],
+            [ B.b_kw "Let"; B.b_space;
+              B.Object ([], P.Mi([],get_name d.Con.def_name));
+              B.Text([]," = ");
+              term])
 
   and acontext2pres ac continuation indent =
     List.fold_right
@@ -360,7 +347,7 @@ and proof2pres term2pres p =
     else if (conclude.Con.conclude_method = "FalseInd") then
       falseind conclude
     else if (conclude.Con.conclude_method = "Rewrite") then
-      let justif1, justif2 = 
+      let justif1,justif2 = 
         (match (List.nth conclude.Con.conclude_args 6) with
            Con.ArgProof p -> justification term2pres p
          | _ -> assert false) in
@@ -377,9 +364,28 @@ and proof2pres term2pres p =
           (B.b_kw "rewrite");
           B.b_space; term1;
           B.b_space; (B.b_kw "with");
-          B.b_space; term2; 
-          B.b_space; justif1]) ::
-          match justif2 with None -> [] | Some j -> [B.indent j])
+          B.b_space; term2;
+          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
@@ -483,10 +489,7 @@ and proof2pres term2pres p =
                     (match e with 
                        `Declaration h 
                      | `Hypothesis h -> 
-                         let name = 
-                           (match h.Con.dec_name with
-                              None -> "NO NAME???"
-                           | Some n ->n) in
+                         let name = get_name h.Con.dec_name in
                          [B.b_space;
                           B.Object ([], P.Mi ([],name));
                           B.Text([],":");
@@ -588,21 +591,17 @@ and proof2pres term2pres p =
            | _ -> 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.Object ([], P.Mi([],get_name hyp1.Con.dec_name));
                 B.Text([],")");
                 B.skip;
                 term2pres hyp1.Con.dec_type]) in
             let preshyp2 = 
               B.H ([],
                [B.Text([],"(");
-                B.Object ([], P.Mi([],get_name hyp2));
+                B.Object ([], P.Mi([],get_name hyp2.Con.dec_name));
                 B.Text([],")");
                 B.skip;
                 term2pres hyp2.Con.dec_type]) in
@@ -630,22 +629,18 @@ and proof2pres term2pres p =
        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.Object ([], P.Mi([],get_name decl.Con.dec_name));
                 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.Object ([], P.Mi([],get_name hyp.Con.dec_name));
                 B.Text([],")");
                 B.skip;
                 term2pres hyp.Con.dec_type]) in