diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-05-04 10:28:56 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-05-04 12:06:27 +0200 |
commit | 4cc655377e3c73fd3066cd8136d17605f167ef56 (patch) | |
tree | 06f0f4a5999e9caf6cef311910ac6a5387ed06a0 /tactics/eauto.ml | |
parent | 773d95f915996b581b7ea82d9193197649c951a0 (diff) |
Improve documentation of assert / pose proof / specialize.
This commits documents the as clause of specialize and that the
as clause of pose proof is optional.
It also mentions a feature of assert ( := ) that was available
since 8.5 and was mentionned by @herbelin in:
https://github.com/coq/coq/pull/248#issuecomment-297970503
Diffstat (limited to 'tactics/eauto.ml')
0 files changed, 0 insertions, 0 deletions