+(* map_sequent is similar to map_conjectures, but the for the hid
+of the hypothesis, which are preserved instead of generating
+fresh ones. We shall have to adopt a uniform policy, soon or later *)
+
+let map_sequent ((id,n,context,ty):Cic.annconjecture) =
+ let module K = Content in
+ let context' =
+ List.map
+ (function
+ (id,None) -> None
+ | (id,Some (name,Cic.ADecl 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 = id;
+ K.dec_inductive = false;
+ K.dec_aref = get_id t;
+ K.dec_type = t
+ })
+ | (id,Some (name,Cic.ADef 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 = id;
+ K.def_aref = get_id t;
+ K.def_term = t
+ })
+ ) context
+ in
+ (id,n,context',ty)
+;;
+