aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-12-04 17:31:28 +0000
committerGitHub2020-12-04 17:31:28 +0000
commit751afe3f52e52f14cf0972498d84722519dd91e7 (patch)
tree86e38be6578608ee79bbf24f37ae5cdabcafe9f0 /doc
parent4d21a082f4bc1a2a98328abc545a22f448affdf4 (diff)
parentffc0f5992e21a9dab5bead467cb41bbcc7face01 (diff)
Merge PR #13569: typo
Reviewed-by: jfehrle
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/language/extensions/arguments-command.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index 95c5914e47..d178311b4c 100644
--- a/doc/sphinx/language/extensions/arguments-command.rst
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -79,7 +79,7 @@ Setting properties of a function's arguments
`!`
the function will be unfolded only if all the arguments marked with `!`
- evaulate to constructors. See :ref:`Args_effect_on_unfolding`.
+ evaluate to constructors. See :ref:`Args_effect_on_unfolding`.
:n:`@name {? % @scope }`
a *formal parameter* of the function :n:`@reference` (i.e.