diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:02 +0200 |
| commit | c5353cb7118690f7ea5e4a1ac3c02448424b8c03 (patch) | |
| tree | 0fa960e2b4fc7dd78f4398462cad29a6ccfb6a18 /tactics/hipattern.mli | |
| parent | e34d7cbcb5ee5c8888efef439ef264ce01a20824 (diff) | |
Revert "Warn about possible shadowing of a name occurring in a "in" clause."
This reverts commit 46f876a9404844487476415af2e6f6d938558d15.
Diffstat (limited to 'tactics/hipattern.mli')
0 files changed, 0 insertions, 0 deletions