X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicDischarge.mli;h=7d6f630f4ace6a8af204b552871de3112aab5d78;hb=987627a48b2a3c2345d1af2c2a6b1ab78aa90b58;hp=447e2a344e6f6bee851f365b92efb1d26d71d27a;hpb=04f22df647f35080b499b720bca7bc0eb1794c64;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicDischarge.mli b/helm/software/components/cic_proof_checking/cicDischarge.mli
index 447e2a344..7d6f630f4 100644
--- a/helm/software/components/cic_proof_checking/cicDischarge.mli
+++ b/helm/software/components/cic_proof_checking/cicDischarge.mli
@@ -23,12 +23,18 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(* discharges the explicit variables of the given object (with sharing)    *)
-(* the first argument is a map for relocating the uris of the dependencdes *)
+(* discharges the explicit variables of the given object (with sharing)     *)
+(* the first argument is a map for relacating the names of the objects      *)
+(* the second argument is a map for relocating the uris of the dependencdes *)
 val discharge_object:
-   (UriManager.uri -> UriManager.uri) -> Cic.obj -> Cic.obj
+   (string -> string) -> (UriManager.uri -> UriManager.uri) -> 
+   Cic.obj -> Cic.obj
 
 (* applies the previous function to the object at the given uri *)
 (* returns true if the object does not need discharging         *)
 val discharge_uri:
-   (UriManager.uri -> UriManager.uri) -> UriManager.uri -> Cic.obj * bool
+   (string -> string) -> (UriManager.uri -> UriManager.uri) ->
+   UriManager.uri -> Cic.obj * bool
+
+(* if activated prints the received object before and after discharging *)
+val debug: bool ref