diff options
| author |  Zeimer <zzaimer@gmail.com> | 2018-07-14 14:20:25 +0200 |
|---|---|---|
| committer | Zeimer <zzaimer@gmail.com> | 2018-07-19 15:48:37 +0200 |
| commit | bdf65b2516b0dd5f4e1a1c6130fc49ee7712dd07 (patch) | |
| tree | 7ca4c2934943636f017dc1d90116723b4c4c515a /.gitattributes | |
| parent | fc1da651e93c08b281dc224dbbd0284390240a47 (diff) | |
Fixed some typos and grammar errors from section 'The language' of the Reference Manual. Removed all mentions of prodT because it is no longer a separate inductive definition (prod has been living in Type for some time) but rather only a notation for prod needed for compatibility purposes.
Diffstat (limited to '.gitattributes')
0 files changed, 0 insertions, 0 deletions