aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/proof-engine/ssreflect-proof-language.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/proof-engine/ssreflect-proof-language.rst')
-rw-r--r--doc/sphinx/proof-engine/ssreflect-proof-language.rst2
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 16d0420ec..ab52c2ce7 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1484,7 +1484,7 @@ The abstract tactic
```````````````````
.. tacn:: abstract: {+ d_item}
- :name abstract (ssreflect)
+ :name: abstract (ssreflect)
This tactic assigns an abstract constant previously introduced with the ``[:
name ]`` intro pattern (see section :ref:`introduction_ssr`).