From c52e7083d490a0c163f25513408c4f17a186a22c Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Thu, 11 Jul 2019 09:45:08 +0200 Subject: Update doc/sphinx/proof-engine/ssreflect-proof-language.rst Co-Authored-By: Théo Zimmermann --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit v1.2.3