X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.mli;h=e1dfb82de1e118e8ecda4d89bb06dde1a97abc26;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=10ec4b0d1a8fc14e7d66fc1e13dedfd03e05160b;hpb=2e062d07e358eb95f0dcbec8fcdfbc2a4fb9ae1f;p=helm.git diff --git a/helm/ocaml/cic_omdoc/cic2content.mli b/helm/ocaml/cic_omdoc/cic2content.mli index 10ec4b0d1..e1dfb82de 100644 --- a/helm/ocaml/cic_omdoc/cic2content.mli +++ b/helm/ocaml/cic_omdoc/cic2content.mli @@ -24,10 +24,10 @@ *) val annobj2content : - ids_to_inner_sorts:(string, string) Hashtbl.t -> - ids_to_inner_types:(string, Cic2acic.anntypes) Hashtbl.t -> + ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> + ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> Cic.annobj -> - Cic.annterm Content.cobj + Cic.annterm Content.cobj val map_sequent : Cic.annconjecture -> Cic.annterm Content.conjecture