diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-08 14:59:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-08 15:03:23 +0200 |
| commit | 15e43996b342f2eddf0c6c0bd4166e757589337e (patch) | |
| tree | 24be0b0dce97f48d502581ec88e8744c6f109d00 /ide/wg_MessageView.ml | |
| parent | e9c6d4cbc9973e0c46b8022fcc5a794f363d1e86 (diff) | |
Fixes #7195 (missing freshness condition in Ltac pattern-matching names).
We ensure that all original names in a spine of matched nested binders
are distinct.
Note: This enforces that two binders with same internal names are kept
disjoint but this does not enforce that we shall respect names exactly
as they are printed. Only the original prefix of the internal names
are preserved, not their "0" or "1" etc. suffix.
Diffstat (limited to 'ide/wg_MessageView.ml')
0 files changed, 0 insertions, 0 deletions