diff options
| author | Hugo Herbelin | 2015-10-04 08:19:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:05 +0100 |
| commit | 5f156b28c84a86a978ab150ab5bbac5ad928ada5 (patch) | |
| tree | 423b904c99d877c4efb74a87cb40eca99956ec2d /kernel/cemitcodes.ml | |
| parent | 5cdf3cfc8ddfb9854534fadc1a08019e9c472590 (diff) | |
RefMan, ch. 4: Consistently using "constant" for names assumed or defined
in global environment and "variable" for names assumed or defined in
local context.
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions