diff options
| -rw-r--r-- | proofs/proof.ml | 9 |
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 |