diff options
| author | Hugo Herbelin | 2018-10-16 15:28:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-31 18:22:41 +0100 |
| commit | ba110aab290cecc8847f3bc3b8396d5d1b9493b0 (patch) | |
| tree | aa5908c85f85997bbe03423826ad512ea14761b2 /dev/ci/docker | |
| parent | 2a93216a3851688dd29c06a29c6d1442898faab8 (diff) | |
Partial fix of #8706 (tactic-in-term sensitive to seemingly unrelated scopes).
We compute the binding to tactic-in-term once for all in the right
scopes before interpreting the tactic.
An alternative would have been to surround the constr_expr by
CDelimiters to simulate its interpretation in the expected scopes
(though this would not have worked for temporary scopes).
Diffstat (limited to 'dev/ci/docker')
0 files changed, 0 insertions, 0 deletions