diff options
Diffstat (limited to 'doc/sphinx/language/extensions/implicit-arguments.rst')
| -rw-r--r-- | doc/sphinx/language/extensions/implicit-arguments.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index f8375e93ce..9457505feb 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -115,7 +115,7 @@ application will include that argument. Otherwise, the argument is *non-maximally inserted* and the partial application will not include that argument. Each implicit argument can be declared to be inserted maximally or non -maximally. In Coq, maximally inserted implicit arguments are written between curly braces +maximally. In |Coq|, maximally inserted implicit arguments are written between curly braces "{ }" and non-maximally inserted implicit arguments are written in square brackets "[ ]". .. seealso:: :flag:`Maximal Implicit Insertion` |