Fix (somewhat obsolete) [Existential] command, which conflicted with the shelf.

When an evar was instantiated it failed to disapear from the shelf. It had the consequence of stopping Qed from happening.

Fixes test-suite/success/apply.v

1 files changed, 7 insertions, 2 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 5654e464a..8dc9184b8 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -368,7 +368,12 @@ module V82 = struct
 
   let instantiate_evar n com pr =
     let sp = pr.proofview in
-    let new_proofview = Proofview.V82.instantiate_evar n com sp in
-    { pr with proofview = new_proofview }
+    let proofview = Proofview.V82.instantiate_evar n com sp in
+    let shelf =
+      List.filter begin fun g ->
+        Evd.is_undefined (Proofview.return proofview) g
+      end pr.shelf
+    in
+    { pr with proofview ; shelf }
 
 end