]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic_exportation/cicExportation.mli
milestone in basic_2, λδ-2A reconstructed
[helm.git] / helm / software / components / cic_exportation / cicExportation.mli
index 07c2b88455a0e3c069552ec48bda1e4919906bb6..4d1c82c868ad19816e0a7c00142d7c54819f847c 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_uri obj *)
+val ppobj : string -> Cic.obj -> string