From 37daa227f906a30b6d142e03f7589961476ce50d Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 23 Sep 2005 14:34:35 +0000 Subject: [PATCH] "verbose" argument of remove is now optional (default false) --- helm/matita/matitaSync.ml | 2 +- helm/matita/matitaSync.mli | 6 ++++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index fc952ba4f..95dab0360 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -288,7 +288,7 @@ let time_travel ~present ~past = let last_baseuri = ref "" -let remove ~verbose uri = +let remove ?(verbose=false) uri = let derived_uris_of_uri uri = UriManager.innertypesuri_of_uri uri :: UriManager.univgraphuri_of_uri uri :: diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli index 9dd13529c..f3906fb8b 100644 --- a/helm/matita/matitaSync.mli +++ b/helm/matita/matitaSync.mli @@ -46,5 +46,7 @@ val set_proof_aliases : (* removes the object from DB, Disk, CoercionsDB, CicEnvironment, getter * asserts the uri is resolved to file:// so it is only for - * user's objects *) -val remove: verbose:bool -> UriManager.uri -> unit + * user's objects + * @param verbose defaults to false *) +val remove: ?verbose:bool -> UriManager.uri -> unit + -- 2.39.2