diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-12 18:27:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-12 18:46:39 +0200 |
| commit | 0222f685ebdd55a1596d6689b96ebb86454ba1a7 (patch) | |
| tree | a4a399bd1aeed5f047ccf1ad7c40573c7384e6aa /proofs/proof.ml | |
| parent | 112e974ec90b2afc51a7cffeba49e5777f3ea80f (diff) | |
| parent | 5dd690ee5975262d34d8dcc44191138c8d326f65 (diff) | |
Merge branch 'v8.5' into 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 5fe29653d..5c963d53e 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) |