evd: restrict_evar with candidates, can raise NoCandidatesLeft

When restricting an evar with candidates, raise an exception if this
restriction would leave the evar without candidates, i.e. unsolvable.

- evarutil: mark restricted evars as "cleared"

They would otherwise escape being catched by the [advance] function
of clenv, and result in dangling evars not being registered to the shelf.

- engine: restrict_evar marks it cleared, update the future goals

We make the new evar a future goal and remove the old one.
If we did nothing, [unshelve tac] would work correctly as it
uses [Proofview.advance] to find the shelved goals, going through
the cleared evar. But [Unshelve] would fail as it expects only
undefined evars on the shelf and throws away the defined ones.

0 files changed, 0 insertions, 0 deletions