fixed some TODO in content2pres

[helm.git] / helm / ocaml / cic_transformations / content2pres.ml

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index fdffe82760b840622a2f33829903e7d13abee456..1429826479f0cd5f87f6f715ca931eeab8e09aa9 100644 (file)
--- 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,10 +320,6 @@ and proof2pres term2pres p =
                    term])
             | None -> 
                 prerr_endline "NO NAME!!"; assert false) 
-      | `Joint ho -> assert false (*
-        B.H ([],
-        (B.Text ([],"JOINT ")
-        :: List.map ce2pres ho.Content.joint_defs)) *)
 
   and acontext2pres ac continuation indent =
     let module Con = Content in
@@ -505,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 
@@ -541,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