diff options
| author |  Matej Kosik <matej.kosik@inria.fr> | 2016-10-19 16:51:18 +0200 |
|---|---|---|
| committer | Matej Kosik <matej.kosik@inria.fr> | 2016-10-20 13:10:42 +0200 |
| commit | f514eb9a44e1c3f7098e79e745c24976e226647d (patch) | |
| tree | e1c4d57cdb830dab333cb45ae2c8d5c92a37911c /.gitignore | |
| parent | 102e62afb98903c7c6be667aa9641dc7be4ca34d (diff) | |
CLEANUP: Namegen.to_avoid
This function does the same thing as "Names.Id.List.mem" so:
- I deleted the "Namegen.to_avoid" function and
- replaced all calls of "Namegen.to_avoid" to calls of "Names.Id.List.mem"
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions