diff options
| author | Matthieu Sozeau | 2016-10-12 11:22:53 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-10-12 11:22:53 +0200 |
| commit | 6e49be2c03f11f412d17e41ca2e74232d12d915c (patch) | |
| tree | e8a55b1349d84ba35856b5fd764ed4023a7f1d95 /proofs/proof.ml | |
| parent | 6d55121c90ec50319a3de6a6907726fbcdc2f835 (diff) | |
| parent | 2bcae5b7a22019718973f65cafd271f735d3d85b (diff) | |
Merge remote-tracking branch 'git/bug5123' into v8.5
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 0489305aa7..1f094b3391 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -343,13 +343,20 @@ let run_tactic env tac pr = they to be marked as unresolvable. *) let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in let retrieved = undef (List.rev (Evd.future_goals sigma)) in - let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in + let to_shelve = undef to_shelve in + let shelf = (undef pr.shelf)@retrieved@to_shelve in let proofview = List.fold_left Proofview.Unsafe.mark_as_goal tacticced_proofview retrieved 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) |