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 | |
| 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')
| -rw-r--r-- | doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 5 |
2 files changed, 8 insertions, 1 deletions
diff --git a/doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst b/doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst new file mode 100644 index 0000000000..8d1564533d --- /dev/null +++ b/doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst @@ -0,0 +1,4 @@ +- **Added:** + SSReflect intro pattern ltac views ``/[dup]``, ``/[swap]`` and ``/[apply]`` + (`#13317 <https://github.com/coq/coq/pull/13317>`_, + by Cyril Cohen). 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 `````````````` |