diff options
| author |  Matej Kosik <matej.kosik@inria.fr> | 2017-02-02 10:04:16 +0100 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-04-20 13:11:50 +0200 |
| commit | b3ef24e5008c70801d272aa77251ab0bf4b46855 (patch) | |
| tree | 544c7fc7aea88230080bb46ccf7c22426c59b90a /kernel/names.ml | |
| parent | c86c6558fcf7f8dc4a17aceed24f68f756f28ea9 (diff) | |
correcting a typo in a comment
Diffstat (limited to 'kernel/names.ml')
0 files changed, 0 insertions, 0 deletions