diff options
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 2ee006631a..e9f93d0c8f 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -386,12 +386,7 @@ let run_tactic env tac pr = let sigma = Proofview.return proofview 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 proofview = Proofview.Unsafe.mark_as_unresolvables 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),result |