Dear Luiz, thank you very much for having taken the time to report this problem.
However, I think that this is a normal behavior. It happens when your proof is no longer compatible with the proof obligation (e.g., the first applied rule references a goal which is different from the current one).
However, until you save the new proof, your old proof is still there on the hard-disk and you can inspect it using the proof skeleton view. You even can copy parts of the old proof tree with copy/paste into the new proof.
If I have misunderstood you, do not hesitate to reopen this bug and give more details.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
I will describe the scenario where it happen.
Being in the proving perspective, finish a proof (green face), press save, and in this moment the proof is prune.
There is not any change in the model that can cause the invalidation of the proof. it is simply when save the proof.
bets regards
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Could you please attach a Rodin project archive to this ticket and indicate a proof obligation that exhibits this behavior, so that we can investigate it ?
Cheers,
Laurent.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Dear Luiz, thank you very much for having taken the time to report this problem.
However, I think that this is a normal behavior. It happens when your proof is no longer compatible with the proof obligation (e.g., the first applied rule references a goal which is different from the current one).
However, until you save the new proof, your old proof is still there on the hard-disk and you can inspect it using the proof skeleton view. You even can copy parts of the old proof tree with copy/paste into the new proof.
If I have misunderstood you, do not hesitate to reopen this bug and give more details.
Hello Lauren,
I will describe the scenario where it happen.
Being in the proving perspective, finish a proof (green face), press save, and in this moment the proof is prune.
There is not any change in the model that can cause the invalidation of the proof. it is simply when save the proof.
bets regards
Dear Luis,
your scenario denotes really a bug.
Could you please attach a Rodin project archive to this ticket and indicate a proof obligation that exhibits this behavior, so that we can investigate it ?
Cheers,
Laurent.
This is indeed a bug, but without additional input, we have no way to reproduce it, nor fix it.