snapshot (first version in which some extensions work, e.g. infix +)

[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 aaf4512565e3ee30b479dc6b30c62efbb5021407..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;
                   }
                 ];
@@ -955,6 +958,7 @@ and
       fun (_,n,b,ty,l) ->
         `Inductive
           { K.inductive_id = gen_id inductive_prefix seed;
+            K.inductive_name = n;
             K.inductive_kind = b;
             K.inductive_type = ty;
             K.inductive_constructors = build_constructors seed l