From ea0444233d08b624c2e9caaee74ea8f3b6625710 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 27 Nov 2014 17:10:46 +0100 Subject: 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 --- proofs/proof.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'proofs/proof.ml') 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 -- cgit v1.2.3