diff options
| author | Théo Zimmermann | 2017-05-04 10:28:56 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-05-04 12:06:27 +0200 |
| commit | 4cc655377e3c73fd3066cd8136d17605f167ef56 (patch) | |
| tree | 06f0f4a5999e9caf6cef311910ac6a5387ed06a0 /interp/implicit_quantifiers.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 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions