diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index fc08500613..1b9e3ce0f3 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2929,7 +2929,7 @@ facts. If an :token:`ident` is prefixed with the ``@`` mark, then a let-in redex is created, which keeps track if its body (if any). The syntax -``(ident := c_pattern)`` allows to generalize an arbitrary term using a +:n:`(@ident := @c_pattern)` allows to generalize an arbitrary term using a given name. Note that its simplest form ``(x := y)`` is just a renaming of ``y`` into ``x``. In particular, this can be useful in order to simulate the generalization of a section variable, otherwise not allowed. Indeed |