diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-25 15:01:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:55:49 +0200 |
| commit | 46f876a9404844487476415af2e6f6d938558d15 (patch) | |
| tree | 0aa9dee30e64daca85cd3de427d47166bb345736 /ltac/ltac.mllib | |
| parent | 7e613daf7c71a4180725bddb40151c2b5a6348f4 (diff) | |
Warn about possible shadowing of a name occurring in a "in" clause.
Diffstat (limited to 'ltac/ltac.mllib')
0 files changed, 0 insertions, 0 deletions