diff options
| author | Hugo Herbelin | 2017-09-23 16:18:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-09-23 16:23:54 +0200 |
| commit | 22a3a79f32d5f795143bd808810aba890c630313 (patch) | |
| tree | ea3cb660d8beafa3aca5cb472a5f876e906f510f /API | |
| parent | 2f3cd62d5118efe95330ddc06fdb43ee717ef993 (diff) | |
Discharge.ml: cosmetic renaming of some variables.
The point is to emphasize stronglier when we are talking about
contexts or about arguments.
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions