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, 6 insertions, 0 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 770e31fea..67a812987 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -212,6 +212,9 @@ let clear_dependency_msg env sigma id err inglobal =
       str "Cannot remove " ++ Id.print id ++
       strbrk " without breaking the typing of " ++
       Printer.pr_existential env sigma ev ++ str"."
+  | Evarutil.NoCandidatesLeft ev ->
+      str "Cannot remove " ++ Id.print id ++ str " as it would leave the existential " ++
+      Printer.pr_existential_key sigma ev ++ str" without candidates."
 
 let error_clear_dependency env sigma id err inglobal =
   user_err (clear_dependency_msg env sigma id err inglobal)
@@ -228,6 +231,9 @@ let replacing_dependency_msg env sigma id err inglobal =
       str "Cannot change " ++ Id.print id ++
       strbrk " without breaking the typing of " ++
       Printer.pr_existential env sigma ev ++ str"."
+  | Evarutil.NoCandidatesLeft ev ->
+      str "Cannot change " ++ Id.print id ++ str " as it would leave the existential " ++
+      Printer.pr_existential_key sigma ev ++ str" without candidates."
 
 let error_replacing_dependency env sigma id err inglobal =
   user_err (replacing_dependency_msg env sigma id err inglobal)