]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8730af0) | patch
MatitaSync.remove must remove the objects also from the environment.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 21 Jul 2005 12:42:58 +0000 (12:42 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 21 Jul 2005 12:42:58 +0000 (12:42 +0000)
commitd35d134356645a09eb72db6e484f3df583123af1
treeb98b55f237feaf1858a16b7539610f609f8fe11ctree | snapshot
parent8730af050d2d27d9aa0d4de42d3b0278a0a9ba6ccommit | diff
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 diff | blob | history
helm/matita/matitaSync.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.