diff options
| author | Hugo Herbelin | 2016-05-14 21:05:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-09 15:38:49 +0200 |
| commit | 715f547816addf3e2e9dc288327fcbcee8c6d47f (patch) | |
| tree | 4fb49ebc62e8090c336b160c83ceea0c36ee11fd /kernel | |
| parent | 92aea31430f9d0e8a0fc8f0d6b7fd1a221768f6c (diff) | |
Improve the interpretation scope of arguments of an ltac match.
Now, type_scope is consistently used whether it is an hypothesis or
the conclusion, and consistently not used when in "context".
The question of a compatibility support, e.g., as suggested by Jason,
using a scope is still open though.
See reports #3050 and #4398.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions