X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=1429826479f0cd5f87f6f715ca931eeab8e09aa9;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=ef79ab4ad254aebac239a96dbf31f83281565e59;hpb=600584314336cb13922438d1e6bcf6044314db72;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index ef79ab4ad..142982647 100644
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -254,17 +254,33 @@ and proof2pres term2pres p =
             (fun ce continuation ->
               let xref = get_xref ce in
               B.V([Some "helm", "xref", xref ],
-                [B.H([Some "helm", "xref", "ce_"^xref],[ce2pres ce]);
+                [B.H([Some "helm", "xref", "ce_"^xref],
+                     [ce2pres_in_proof_context_element ce]);
                  continuation])) tl continuation in
          let hd_xref= get_xref hd in
          B.V([],
              [B.H([Some "helm", "xref", "ce_"^hd_xref],
-               [ce2pres hd]);
+               [ce2pres_in_proof_context_element hd]);
              continuation'])
-         
-  and ce2pres =
+        
+  and ce2pres_in_joint_context_element = function
+    | `Inductive _ -> assert false (* TODO *)
+    | (`Declaration _) as x -> ce2pres x
+    | (`Hypothesis _) as x  -> ce2pres x
+    | (`Proof _) as x       -> ce2pres x
+    | (`Definition _) as x  -> ce2pres x
+  
+  and ce2pres_in_proof_context_element = function 
+    | `Joint ho -> 
+      B.H ([],(List.map ce2pres_in_joint_context_element ho.Content.joint_defs))
+    | (`Declaration _) as x -> ce2pres x
+    | (`Hypothesis _) as x  -> ce2pres x
+    | (`Proof _) as x       -> ce2pres x
+    | (`Definition _) as x  -> ce2pres x
+  
+  and ce2pres = 
     let module Con = Content in
-      function
+    function 
         `Declaration d -> 
           (match d.Con.dec_name with
               Some s ->
@@ -304,8 +320,6 @@ and proof2pres term2pres p =
                    term])
             | None -> 
                 prerr_endline "NO NAME!!"; assert false) 
-      | `Joint ho -> 
-            B.Text ([],"jointdef")
 
   and acontext2pres ac continuation indent =
     let module Con = Content in
@@ -380,7 +394,11 @@ and proof2pres term2pres p =
       let arg = 
         (match conclude.Con.conclude_args with 
            [Con.Term t] -> term2pres t
-         | _ -> assert false) in
+         | [Con.Premise p] -> 
+             (match p.Con.premise_binder with
+             | None -> assert false; (* unnamed hypothesis ??? *)
+             | Some s -> B.Text([],s))
+         | err -> assert false) in
       (match conclude.Con.conclude_conclusion with 
          None ->
           B.b_h [] [B.b_kw "Consider"; B.b_space; arg]
@@ -499,7 +517,7 @@ and proof2pres term2pres p =
                B.Text ([],"a proof???")
            | Con.ArgMethod s -> 
                B.Text ([],"a method???")) in
-        (make_concl "we proceede by cases on" case_arg) in
+        (make_concl "we proceed by cases on" case_arg) in
      let to_prove =
         (make_concl "to prove" proof_conclusion) in
      B.V 
@@ -535,7 +553,7 @@ and proof2pres term2pres p =
                B.Text ([],"a proof???")
            | Con.ArgMethod s -> 
                B.Text ([],"a method???")) in
-        (make_concl "we proceede by induction on" arg) in
+        (make_concl "we proceed by induction on" arg) in
      let to_prove =
         (make_concl "to prove" proof_conclusion) in
      B.V