diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 64864bb195..b3ebb4d8df 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1571,8 +1571,8 @@ implicitly applied to the implicit arguments it is waiting for: one says that the implicit argument is maximally inserted. Each implicit argument can be declared to be inserted maximally or non -maximally. In Coq, maximally inserted implicits are written between curly braces -"{ }" and non maximally inserted implicits are written in square brackets "[ ]". +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` @@ -1895,8 +1895,8 @@ Combining manual declaration and automatic declaration ++++++++++++++++++++++++++++++++++++++++++++++++++++++ When some arguments are manually specified implicit with binders in a definition -and the automatic declaration mode in on, the manual implicits are added to the -automatic ones. +and the automatic declaration mode in on, the manual implicit arguments are added to the +automatically declared ones. In that case, and when the flag :flag:`Maximal Implicit Insertion` is set to off, some trailing implicit arguments can be inferred to be non maximally inserted. In |