-let build_def_item seed context metasenv id n t ty =
- let module K = Content in
-(*
- try
- let sort = Hashtbl.find ids_to_inner_sorts id in
- if sort = `Prop then
- (let p =
- (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
- in
- `Proof p;)
- else
-*)
- `Definition
- { K.def_name = Some n;
- K.def_id = gen_id definition_prefix seed;
- K.def_aref = id;
- K.def_term = t;
- K.def_type = ty
- }
-(*
- with
- Not_found -> assert false
-*)
-
-let build_decl_item seed id n s =
- let module K = Content in
-(*
- let sort =
- try
- Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id))
- with Not_found -> None
- in
- match sort with
- | Some `Prop ->
- `Hypothesis
- { K.dec_name = name_of n;
- K.dec_id = gen_id declaration_prefix seed;
- K.dec_inductive = false;
- K.dec_aref = id;
- K.dec_type = s
- }
- | _ ->
-*)
- `Declaration
- { K.dec_name = Some n;
- K.dec_id = gen_id declaration_prefix seed;
- K.dec_inductive = false;
- K.dec_aref = id;
- K.dec_type = s
- }
-;;
-