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 /pretyping | |
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 'pretyping')
0 files changed, 0 insertions, 0 deletions