diff options
| author | herbelin | 2009-12-30 12:02:32 +0000 |
|---|---|---|
| committer | herbelin | 2009-12-30 12:02:32 +0000 |
| commit | 306d1be283442c361aa26d000d339f3f4dfbeab9 (patch) | |
| tree | 5fdec06c70ef551f8b775988820fb07c7538e29f /dev/base_include | |
| parent | 77d86619f5f557de52a391f6811bacd73c01580b (diff) | |
Fixing bug #2146 (broken selection of occurrences in "change").
In trunk the different possible combinations of "at" and "in" with
occurrences are taken into account.
In 8.2 branch, it remains fragile (syntaxes that were accepted remain
accepted and a message warns if the occurrences coming after the
"with" are not taken into account).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12614 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions