diff options
| author | Zeimer | 2018-07-14 14:20:25 +0200 |
|---|---|---|
| committer | Zeimer | 2018-07-19 15:48:37 +0200 |
| commit | bdf65b2516b0dd5f4e1a1c6130fc49ee7712dd07 (patch) | |
| tree | 7ca4c2934943636f017dc1d90116723b4c4c515a /plugins | |
| 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 'plugins')
0 files changed, 0 insertions, 0 deletions