diff options
| author | Hugo Herbelin | 2015-10-22 18:22:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-14 22:05:49 +0200 |
| commit | a88f5f162272ced5fb2b8ea555756b8fc51b939a (patch) | |
| tree | eecdbf3d1b1f38e1c4c3799ec2f210461dd8cbcc /lib | |
| parent | 87a81fd7e6ff6b45c76690471eb671ba4b005338 (diff) | |
This is an attempt to clarify terminology in choosing variable names
in file indtypes.ml so that it is easier to follow what the code is
doing.
This is a purely alpha-renaming commit (if no mistakes).
Note: was submitted as pull request #116.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions