diff options
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 38fcdd6e5f..c427c07b93 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -373,7 +373,7 @@ let run_tactic env tac pr = Proofview.tclEVARMAP >>= fun sigma -> (* Already solved goals are not to be counted as shelved. Nor are they to be marked as unresolvable. *) - let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) (Evd.save_future_goals sigma) in + let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) sigma in let retrieved,retrieved_given_up = Evd.extract_given_up_future_goals retrieved in (* Check that retrieved given up is empty *) if not (List.is_empty retrieved_given_up) then |