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.

1 files changed, 3 insertions, 0 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 0c9c3a29b..7e0c397b2 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -171,6 +171,8 @@ let evar_context evi = named_context_of_val evi.evar_hyps
 let evar_filtered_context evi =
   Filter.filter_list (evar_filter evi) (evar_context evi)
 
+let evar_candidates evi = evi.evar_candidates
+
 let evar_hyps evi = evi.evar_hyps
 
 let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with
@@ -620,6 +622,7 @@ let merge_universe_context evd uctx' =
 let set_universe_context evd uctx' =
   { evd with universes = uctx' }
 
+(* TODO: make unique *)
 let add_conv_pb ?(tail=false) pb d =
   (** MS: we have duplicates here, why? *)
   if tail then {d with conv_pbs = d.conv_pbs @ [pb]}