X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.mli;fp=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.mli;h=ff75618f84f2b41413c54e002decde233bf5a0c3;hb=18ab6500105671c07f65430be5c899732fc101c3;hp=2dd0a2f319652c0995b5230369ed582596df8aff;hpb=ec11b4f9daa87bb3aa8f48968c5712d39a0e5374;p=helm.git diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli index 2dd0a2f31..ff75618f8 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.mli +++ b/helm/ocaml/cic_omdoc/cic2acic.mli @@ -37,19 +37,6 @@ val string_of_sort: sort_kind -> string val sort_of_string: string -> sort_kind val sort_of_sort: Cic.sort -> sort_kind -val acic_of_cic_context' : - int ref -> (* seed *) - (Cic.id, Cic.term) Hashtbl.t -> (* ids_to_terms *) - (Cic.id, Cic.id option) Hashtbl.t -> (* ids_to_father_ids *) - (Cic.id, sort_kind) Hashtbl.t -> (* ids_to_inner_sorts *) - (Cic.id, anntypes) Hashtbl.t -> (* ids_to_inner_types *) - Cic.metasenv -> (* metasenv *) - Cic.context -> (* context *) - Cic.id list -> (* idrefs *) - Cic.term -> (* term *) - Cic.term option -> (* expected type *) - Cic.annterm (* annotated term *) - val acic_object_of_cic_object : ?eta_fix: bool -> (* perform eta_fixing; default: true*) Cic.obj -> (* object *)