]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/cic2content.mli
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_omdoc / cic2content.mli
index 10ec4b0d1a8fc14e7d66fc1e13dedfd03e05160b..e1dfb82de1e118e8ecda4d89bb06dde1a97abc26 100644 (file)
  *)
 
 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