diff options
| author | Florent Hivert | 2019-07-11 09:45:08 +0200 |
|---|---|---|
| committer | GitHub | 2019-07-11 09:45:08 +0200 |
| commit | c52e7083d490a0c163f25513408c4f17a186a22c (patch) | |
| tree | 6b4074cc018972a2aba34bcdf2a7f2d81f0a1dcc /doc/sphinx/proof-engine | |
| parent | ef5a7e27f70013a8aa953eef8fd302ce54d23bc3 (diff) | |
Update doc/sphinx/proof-engine/ssreflect-proof-language.rst
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Diffstat (limited to 'doc/sphinx/proof-engine')
| -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 |