Menu
▾
▴
#707 Not refreshing current proof node when model changes
This bug is present in Rodin 2.8, and probably before.
When editing a proof, if the model is changed, saved and built, the current proof node is not refreshed: we have to manually select another proof node in the proof tree, then select back the proof node.
For instance, hypotheses that have changed or disappeared are still displayed unchanged.
However this has no incidence on proof integrity, as trying to use a hypothesis that has changed or disappeared will fail.
This bug does not happen if the model and the proof editor are displayed side to side (i.e, the proof editor is correctly refreshed in this case).
