On session reload, proved goals without any transformation are not marked as obsolete
Consider the following example:
module M
goal G : true
end
We normally prove the VC for goal G by directly calling Alt-Ergo, without any transformation. Now, we save and quit the session.
Next, we change the very same file as follows:
module M
goal G : false
end
When we reload the session, goal G is still marked as proved and not as obsolete (I would expect the latter to happen).
We do not observe this behavior if some transformation is used. Consider the following example:
module M
use int.Int
goal G : 1 + 1 = 2 /\ true
end
We call split_vc
and then call Alt-Ergo on the generated goal. We save and quit the session. We do the following change:
module M
use int.Int
goal G : 1 + 1 = 2 /\ false
end
When we reload the session, now the proof attempt is marked as obsolete.