]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/content2cic.mli
Interface change: only cobj2obj is exposed.
[helm.git] / helm / ocaml / cic_omdoc / content2cic.mli
index a1c19fa578bcfb6c60ae19df4b6dcd0a07be43f5..9bb6509cc23da41c4e5fe7fd84495aeb4da8fd68 100644 (file)
@@ -32,4 +32,4 @@
 (*                                                                        *)
 (**************************************************************************)
 
-val proof2cic : Cic.annterm Content.proof -> Cic.term
+val cobj2obj : Cic.annterm Content.cobj -> Cic.obj