diff options
| author | Arnaud Spiwack | 2014-08-05 15:51:16 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-05 16:52:14 +0200 |
| commit | 664b3cba1e8d326382ca981aa49fdf00edd429e6 (patch) | |
| tree | 462c7a7e2cc4c0becb5259feb1c25ca10bcdd5c9 /stm/asyncTaskQueue.ml | |
| parent | 1624735620d7e375a124231fea94648eac0da342 (diff) | |
Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].
When "entering" in a goal, the environment observed by [tclENV] is changed (in the scope of the goal) to be that of the goal.
I'm not entirely sure it is the right semantics. But it allows to write tactics which are agnostic of whether they are run in a goal or not.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions