aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
diff options
context:
space:
mode:
authorGravatar Zeimer <zzaimer@gmail.com>2018-07-15 15:18:51 +0200
committerGravatar Zeimer <zzaimer@gmail.com>2018-07-20 18:31:07 +0200
commit9f61a0ff9822269fa3cb949203b4048ffc62a601 (patch)
tree70b69f43061a25dfd7905d16a76f8fde24411553 /grammar
parentd8cd9ba6d56d32eb8aa383bca9198a18517e82d3 (diff)
Fixed many spelling and grammar errors in the chapters 'Vernacular commands', 'Proof handling' and 'Tactics' of the Reference Manual.
Fixed some more serious errors related to tactics functional induction, unfold, hnf and red. Added some error messages and remarks for tactics btauto, rtauto and red.
Diffstat (limited to 'grammar')
0 files changed, 0 insertions, 0 deletions