X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=0f23afb5691b7721b0b67b2f9e73ce267d3a9147;hb=f15a13bab100064a4da238cede323b8d4568c174;hp=58ef34c871cd49cdc43c2302e73e4fa321c17ebf;hpb=058acfd867b172244c9beb95c11fdd2ad270f5a0;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 58ef34c87..0f23afb56 100644
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -834,30 +834,28 @@ let map_conjectures
  let context' =
   List.map
    (function
-       (id,None) as item -> item
+       (id,None) -> None
      | (id,Some (name,Cic.ADecl t)) ->
-         id,
-          Some
-           (* We should call build_decl_item, but we have not computed *)
-           (* the inner-types ==> we always produce a declaration      *)
-           (`Declaration
-             { K.dec_name = name_of name;
-               K.dec_id = gen_id declaration_prefix seed; 
-               K.dec_inductive = false;
-               K.dec_aref = get_id t;
-               K.dec_type = t
-             })
+         Some
+          (* We should call build_decl_item, but we have not computed *)
+          (* the inner-types ==> we always produce a declaration      *)
+          (`Declaration
+            { K.dec_name = name_of name;
+              K.dec_id = gen_id declaration_prefix seed; 
+              K.dec_inductive = false;
+              K.dec_aref = get_id t;
+              K.dec_type = t
+            })
      | (id,Some (name,Cic.ADef t)) ->
-         id,
-          Some
-           (* We should call build_def_item, but we have not computed *)
-           (* the inner-types ==> we always produce a declaration     *)
-           (`Definition
-              { K.def_name = name_of name;
-                K.def_id = gen_id definition_prefix seed; 
-                K.def_aref = get_id t;
-                K.def_term = t
-              })
+         Some
+          (* We should call build_def_item, but we have not computed *)
+          (* the inner-types ==> we always produce a declaration     *)
+          (`Definition
+             { K.def_name = name_of name;
+               K.def_id = gen_id definition_prefix seed; 
+               K.def_aref = get_id t;
+               K.def_term = t
+             })
    ) context
  in
   (id,n,context',ty)