]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4ac6edc) | patch
New function replace to be used in place of time_travel every time the user
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 15 Jul 2011 14:40:34 +0000 (14:40 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 15 Jul 2011 14:40:34 +0000 (14:40 +0000)
commit2c977fe8fdfb6930ed73c6ef806ed35423f4ab6c
tree1aa0d59573f4a4c39b1d561cb9235548783f0a16tree | snapshot
parent4ac6edc22587ae3c19c36925dbf003c2e111fffacommit | diff
New function replace to be used in place of time_travel every time the user
switches to a new tab. In this way, every tab is independent and it only sees
the objects defined in that tab. This fixes the following bug: in tab A go
down; go down in tab B; go up in tab A (at this point also the objects declared
in B where removed); do something in B or go up in B (BOOM))
matita/components/ng_library/nCicLibrary.ml diff | blob | history
matita/components/ng_library/nCicLibrary.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.