During a refinement, the user may have done some errors: a wrong refinement step,
an inadequate commentary insertion, or wrong proof obligation marking. CRefine offers the choice
to undo the updates done to the development. For that, we must choose the Undo option in the Edit menu, or click on the
button.
Depending on the step that has been undone, any of the windows may be updated. It may also change the terms that can be collected.
CRefine also allows steps of loaded development to be undone/redone. This helps users to go back in previous developments, helping them to understand each one of the refinement steps. Analogously, we may select Redo from the Edit menu in order to redo some undone refinement steps. The button
may be selected for that matter.
The redo functionality yields the same updates as its original action. Hence, the GUI windows can be updated, as well as the terms for collection.
After doing any other action after undoing a previous action, the previous action cannot be redone anymore.
button.
Depending on the step that has been undone, any of the windows may be updated. It may also change the terms that can be collected.
CRefine also allows steps of loaded development to be undone/redone. This helps users to go back in previous developments, helping them to understand each one of the refinement steps. Analogously, we may select Redo from the Edit menu in order to redo some undone refinement steps. The button
may be selected for that matter.
The redo functionality yields the same updates as its original action. Hence, the GUI windows can be updated, as well as the terms for collection.
After doing any other action after undoing a previous action, the previous action cannot be redone anymore.