diff options
| author | Maxime Dénès | 2020-06-11 13:11:21 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-08-26 16:38:34 +0200 |
| commit | 4e59a68fd6f2cd3cdf936c10cdbfeb46fc22ca95 (patch) | |
| tree | 0bdb09f0eae78a88b855ebcff4da3e2a9b363800 /proofs/proof.ml | |
| parent | 4e6b029805a74ea16166da2c5f59f9669fd34eb8 (diff) | |
Better encapsulation of future goals
We try to encapsulate the future goals abstraction in the evar map.
A few calls to `save_future_goals` and `restore_future_goals` are still
there, but we try to minimize them.
This is a preliminary refactoring to make the invariants between the
shelf and future goals more explicit, before giving unification access
to the shelf, which is needed for #7825.
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 |