From d226adf01f20ea946bbeac4d4c5cde75a4d77f32 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 11 Oct 2016 11:57:46 +0200
Subject: Fix bug #5123: mark all shelved evars unresolvable

Previously, some splipped through and were caught by unrelated calls to
typeclass resolution.
---
 proofs/proof.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'proofs/proof.ml')

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 0489305aa7..1f094b3391 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)
-- 
cgit v1.2.3