aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-11-27 17:10:46 +0100
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-11-28 19:21:24 +0100
commitea0444233d08b624c2e9caaee74ea8f3b6625710 (patch)
tree3335f671d8e2cfdc070d510eca730aedb576f1cd /proofs
parent34815f0c8fae4c87798b18f7343c1f1afc3056eb (diff)
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
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proof.ml9
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