fixed some TODO in content2pres

[helm.git] / helm / ocaml / cic_omdoc / cic2content.ml

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;
                   }
                 ];