diff options
| author | Pierre-Marie Pédrot | 2016-10-12 21:14:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-12 21:14:07 +0200 |
| commit | 05ad4f49ac2203dd64dfec79a1fc62ee52115724 (patch) | |
| tree | 920faae7946821c093345fd1804c40336bd9f1c4 /proofs/proof.ml | |
| parent | 8a6c792505160de4ba2123ef049ab45d28873e47 (diff) | |
| parent | 0222f685ebdd55a1596d6689b96ebb86454ba1a7 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 16278b456a..0a3b08c04a 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -351,7 +351,14 @@ let run_tactic env tac pr = Proofview.apply env tac sp in let sigma = Proofview.return proofview in - let shelf = (undef sigma pr.shelf)@retrieved@(undef sigma to_shelve) in + let to_shelve = undef sigma to_shelve in + let shelf = (undef sigma pr.shelf)@retrieved@to_shelve 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) |