X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=81f0683c6390530b1fabcb87437079084c79c77f;hb=2f15a81dcd6e5ada3f1b4fa6300e9a1347c8d12c;hp=aaf4512565e3ee30b479dc6b30c62efbb5021407;hpb=7df065750ec593fb409ae8627f81927397602b9b;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index aaf451256..81f0683c6 100644
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -955,6 +955,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