diff options
| author | Pierre-Marie Pédrot | 2015-12-09 12:01:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-09 12:16:44 +0100 |
| commit | 11eedd379d4b27e73a1999c0aacc2056311e8ba9 (patch) | |
| tree | 63e8eb15f257e16cb9c6d30958ba6be686635dd9 | |
| parent | 8ea758fbb392e270e6a8d2287dbb5b0455d99368 (diff) | |
The unshelve tactical now takes future goals into account.
| -rw-r--r-- | proofs/proofview.ml | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 5981ad32da..452f27ff2b 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -644,12 +644,18 @@ let unshelve l p = let with_shelf tac = let open Proof in - Shelf.get >>= fun shelf -> - Shelf.set [] >> + Pv.get >>= fun pv -> + let { shelf; solution } = pv in + Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >> tac >>= fun ans -> - Shelf.get >>= fun gls -> - Shelf.set shelf >> - tclUNIT (gls, ans) + Pv.get >>= fun npv -> + let { shelf = gls; solution = sigma } = npv in + let gls' = Evd.future_goals sigma in + let fgoals = Evd.future_goals solution in + let pgoal = Evd.principal_future_goal solution in + let sigma = Evd.restore_future_goals sigma fgoals pgoal in + Pv.set { npv with shelf; solution = sigma } >> + tclUNIT (CList.rev_append gls' gls, ans) (** [goodmod p m] computes the representative of [p] modulo [m] in the interval [[0,m-1]].*) |