From d35d134356645a09eb72db6e484f3df583123af1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 21 Jul 2005 12:42:58 +0000 Subject: [PATCH] MatitaSync.remove must remove the objects also from the environment. This fixes the following bug: in matita open a file B that depends on A (that gets loaded in the environment); then switch to A without exiting matita. It is now impossible to re-compile A. --- helm/matita/matitaSync.ml | 3 ++- helm/matita/matitaSync.mli | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 2547bbdfc..51007df29 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -266,5 +266,6 @@ let remove ~verbose uri = MatitaMisc.safe_remove (Http_getter.resolve' uri) with Http_getter_types.Key_not_found _ -> ()); remove_coercion uri; - ignore (MatitaDb.remove_uri uri)) + ignore (MatitaDb.remove_uri uri); + CicEnvironment.remove_obj uri) to_remove diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli index 66787ad46..492bc8c3b 100644 --- a/helm/matita/matitaSync.mli +++ b/helm/matita/matitaSync.mli @@ -40,7 +40,7 @@ val alias_diff: from:MatitaTypes.status -> MatitaTypes.status -> val set_proof_aliases : MatitaTypes.status -> DisambiguateTypes.environment -> MatitaTypes.status - (* removes the object from DB, Disk, CoercionsDB, getter + (* 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 -- 2.39.2