aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorThéo Zimmermann2016-10-18 14:23:23 +0200
committerThéo Zimmermann2016-10-18 14:48:53 +0200
commit17ec7a0c875014e5322f6098dcd2014072cde9d8 (patch)
treea889b41e2cec632260f6c5c6df6a3e94dd5e5244 /plugins
parent317ae3b327d201530730ed2cce5f44e8763814d4 (diff)
Improve the documentation of eauto.
Improve the description of what auto/eauto do. These two tactics rely on the simple version of apply/eapply. Since this simple version is available to the end user, it is better to mention it. See also the confusion that such description can create in the thread "Understanding auto" on Coq-Club.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions