diff options
| author | coqbot-app[bot] | 2020-11-12 08:18:34 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-12 08:18:34 +0000 |
| commit | 9dfc627ccac11b46bc11bcc11e9609b952d35fdd (patch) | |
| tree | ffb6080e1783060772b9b2a8f906fc9dbfdfcc30 /doc/sphinx/proof-engine | |
| parent | af42e1bec2df12355725bc79e2060f5d3acd0ce1 (diff) | |
| parent | 7bd93b0d6000766d766da4a73dbe44e4189b2085 (diff) | |
Merge PR #13317: [ssr] intro pattern extensions for dup, swap and apply
Reviewed-by: gares
Ack-by: Zimmi48
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 22544b2018..07c2d268c6 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1647,7 +1647,10 @@ Notations can be used to name tactics, for example Notation "'myop'" := (ltac:(my ltac code)) : ssripat_scope. lets one write just ``/myop`` in the intro pattern. Note the scope -annotation: views are interpreted opening the ``ssripat`` scope. +annotation: views are interpreted opening the ``ssripat`` scope. We +provide the following ltac views: ``/[dup]`` to duplicate the top of +the stack, ``/[swap]`` to swap the two first elements and ``/[apply]`` +to apply the top of the stack to the next. Intro patterns `````````````` |