X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicDischarge.mli;h=2e2790a97fb9c3c45604180b80e7a0162ce5cce0;hb=95adf6dc8e29a71adc34e71eafe3f427990126e0;hp=a6b097db2af01c22018662956dc5f5b56da6ae58;hpb=d2d20cd33c42d0897765387042c3779109bbf4fd;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicDischarge.mli b/helm/software/components/cic_proof_checking/cicDischarge.mli index a6b097db2..2e2790a97 100644 --- 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