From 79c45ec7696923c9d2867b094ca30d6af142dbc8 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Fri, 6 Nov 2020 11:32:17 +0100
Subject: Intro pattern extensions for dup, swap and apply

---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx')

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
 ``````````````
-- 
cgit v1.2.3