diff options
| author | Hugo Herbelin | 2015-10-04 08:22:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:05 +0100 |
| commit | ef7264aa6106d0257e1a34f4ecf765279d9b602e (patch) | |
| tree | bd35f2035eb3d92671bf85eec7d6b279fab2fb64 /kernel/cemitcodes.ml | |
| parent | 5f156b28c84a86a978ab150ab5bbac5ad928ada5 (diff) | |
RefMan, ch. 4: Removing confusing paragraph "Constants": in it,
constants are yet given another definition; the reference to other
presentation is more confusing than helpful to me.
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions