+
+let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) =
+ let module K = Content in
+ let ids_to_refs = Hashtbl.create 211 in
+ let register_ref = Hashtbl.add ids_to_refs in
+ let nast_of_cic =
+ nast_of_cic1 ~idref:(idref register_ref) ~output_type:`Term
+ ~subst in
+ let context',_ =
+ List.fold_right
+ (fun item (res,context) ->
+ match item with
+ | name,NCic.Decl 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 = (Some name);
+ K.dec_id = "-1";
+ K.dec_inductive = false;
+ K.dec_aref = "-1";
+ K.dec_type = nast_of_cic ~context t
+ })::res,item::context
+ | name,NCic.Def (t,ty) ->
+ Some
+ (* We should call build_def_item, but we have not computed *)
+ (* the inner-types ==> we always produce a declaration *)
+ (`Definition
+ { K.def_name = (Some name);
+ K.def_id = "-1";
+ K.def_aref = "-1";
+ K.def_term = nast_of_cic ~context t;
+ K.def_type = nast_of_cic ~context ty
+ })::res,item::context
+ ) context ([],[])
+ in
+ ("-1",i,context',nast_of_cic ~context ty), ids_to_refs
+;;
+