diff options
| author | Arnaud Spiwack | 2014-10-16 14:42:20 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-16 15:14:20 +0200 |
| commit | 2d65dac1b0c63039f802d5e92afd389d5e7cc846 (patch) | |
| tree | f1824671df6fda9a2d49bea99b64b6700762ed0a /kernel | |
| parent | ce260a0db279ce09dda70e079ae3c35b49f05ec4 (diff) | |
Put evars remaining after a tactic on the shelf.
Uses the new architecture which allows to keep track of all new evars. The [future_goals] are flushed at the end of the tactics, the [principal_future_goal] is ignored.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions