...

[helm.git] / helm / software / components / cic_proof_checking / cicDischarge.mli

diff --git a/helm/software/components/cic_proof_checking/cicDischarge.mli b/helm/software/components/cic_proof_checking/cicDischarge.mli
index a6b097db2af01c22018662956dc5f5b56da6ae58..2e2790a97fb9c3c45604180b80e7a0162ce5cce0 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicDischarge.mli
+++ b/helm/software/components/cic_proof_checking/cicDischarge.mli
@@ -23,6 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* NOTE. Discharged variables are not well formed. *)
+(*       For internal recursive use only.          *) 
+
 (* 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 *)
@@ -35,3 +38,6 @@ val discharge_object:
 val discharge_uri:
    (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