]> matita.cs.unibo.it Git - helm.git/blobdiff - components/cic_exportation/cicExportation.mli
All exported names are now qualified. This avoids the need for "open" statements.
[helm.git] / components / cic_exportation / cicExportation.mli
index 07c2b88455a0e3c069552ec48bda1e4919906bb6..1f68e4e75e57e8e62e9e8f11f24db67050e0ac16 100644 (file)
@@ -25,4 +25,5 @@
 
 (* $Id: cicPp.ml 7413 2007-05-29 15:30:53Z tassi $ *)
 
-val ppobj : Cic.obj -> string
+(* ppobj current_module_name obj *)
+val ppobj : string -> Cic.obj -> string