* 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 *)
+(* 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 *)
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