diff options
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..4bed302da1 --- /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 cdbae8ade1..39561d837e 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 `````````````` |