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
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.