fixed some TODO in content2pres

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 81f0683c6390530b1fabcb87437079084c79c77f..c7d59aedc6ce91803f496c8affa2b77c37cea8f2 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -600,6 +600,9 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
         let proofs = 
           List.map 
             (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in
+        let fun_name = 
+          List.nth (List.map (fun (_,name,_,_,_) -> name) funs) no 
+        in
         let decreasing_args = 
           List.map (function (_,_,n,_,_) -> n) funs in
         let jo = 
@@ -620,7 +623,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
                 [ K.Premise
                   { K.premise_id = gen_id premise_prefix seed; 
                     K.premise_xref = jo.K.joint_id;
-                    K.premise_binder = Some "tiralo fuori";
+                    K.premise_binder = Some fun_name;
                     K.premise_n = Some no;
                   }
                 ];

diff --git a/helm/ocaml/cic_omdoc/content.mli b/helm/ocaml/cic_omdoc/content.mli
index 9a38ea4be5578d5c1a06fd2dac47d74c94272401..99869b9b47623ab226574da143eb625ec3e5bdfe 100644 (file)
--- a/helm/ocaml/cic_omdoc/content.mli
+++ b/helm/ocaml/cic_omdoc/content.mli
@@ -100,7 +100,7 @@ type 'term proof =
 
 and 'term in_proof_context_element =
        [ 'term decl_context_element
-       | ('term,'term proof) def_context_element
+       | ('term,'term proof) def_context_element 
        | ('term,'term proof) joint_context_element
        ]
 

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