X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_cic_content%2FnTermCicContent.ml;h=5d91cee284a7ab0e73c9e08d1ef1b7ed3de63db9;hb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;hp=dbd6523cf946b302eead79de25beb5fca0037549;hpb=42aa528129728611cae9da02904886522b08f94a;p=helm.git

diff --git a/matita/components/ng_cic_content/nTermCicContent.ml b/matita/components/ng_cic_content/nTermCicContent.ml
index dbd6523cf..5d91cee28 100644
--- a/matita/components/ng_cic_content/nTermCicContent.ml
+++ b/matita/components/ng_cic_content/nTermCicContent.ml
@@ -589,7 +589,7 @@ in
   let res =
    match kind with
     | NCic.Fixpoint (is_rec, ifl, _) -> 
-         (gen_id object_prefix seed, [], conjectures,
+         (gen_id object_prefix seed, conjectures,
             `Joint
               { K.joint_id = gen_id joint_prefix seed;
                 K.joint_kind = 
@@ -599,7 +599,7 @@ in
                 K.joint_defs = List.map (build_fixpoint is_rec seed) ifl
               }) 
     | NCic.Inductive (is_ind, lno, itl, _) ->
-         (gen_id object_prefix seed, [], conjectures,
+         (gen_id object_prefix seed, conjectures,
             `Joint
               { K.joint_id = gen_id joint_prefix seed;
                 K.joint_kind = 
@@ -609,12 +609,12 @@ in
     | NCic.Constant (_,_,Some bo,ty,_) ->
        let ty = nast_of_cic ~context:[] ty in
        let bo = nast_of_cic ~context:[] bo in
-        (gen_id object_prefix seed, [], conjectures,
+        (gen_id object_prefix seed, conjectures,
           `Def (K.Const,ty,
             build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty))
     | NCic.Constant (_,_,None,ty,_) ->
        let ty = nast_of_cic ~context:[] ty in
-         (gen_id object_prefix seed, [], conjectures,
+         (gen_id object_prefix seed, conjectures,
            `Decl (K.Const,
              (*CSC: ??? get_id ty here used to be the id of the axiom! *)
              build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty))