Fix bug #5123: mark all shelved evars unresolvable

Previously, some splipped through and were caught by unrelated calls to
typeclass resolution.

1 files changed, 8 insertions, 1 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 0489305aa..1f094b339 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -343,13 +343,20 @@ let run_tactic env tac pr =
      they to be marked as unresolvable. *)
   let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in
   let retrieved = undef (List.rev (Evd.future_goals sigma)) in
-  let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in
+  let to_shelve = undef to_shelve in
+  let shelf = (undef pr.shelf)@retrieved@to_shelve in
   let proofview =
     List.fold_left
       Proofview.Unsafe.mark_as_goal
       tacticced_proofview
       retrieved
   in
+  let proofview =
+    List.fold_left
+      Proofview.Unsafe.mark_as_unresolvable
+      proofview
+      to_shelve
+  in
   let given_up = pr.given_up@give_up in
   let proofview = Proofview.Unsafe.reset_future_goals proofview in
   { pr with proofview ; shelf ; given_up },(status,info_trace)