diff options
Diffstat (limited to 'doc/sphinx/language/extensions/implicit-arguments.rst')
| -rw-r--r-- | doc/sphinx/language/extensions/implicit-arguments.rst | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index 9457505feb..23ba5f703a 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` @@ -146,7 +146,7 @@ by replacing it with `_`. .. exn:: Cannot infer a term for this placeholder. :name: Cannot infer a term for this placeholder. (Casual use of implicit arguments) - |Coq| was not able to deduce an instantiation of a “_”. + Coq was not able to deduce an instantiation of a “_”. .. _declare-implicit-args: @@ -290,8 +290,8 @@ Controlling contextual implicit arguments .. flag:: Contextual Implicit - By default, |Coq| does not automatically set implicit the contextual - implicit arguments. You can turn this flag on to tell |Coq| to also + By default, Coq does not automatically set implicit the contextual + implicit arguments. You can turn this flag on to tell Coq to also infer contextual implicit argument. .. _controlling-rev-pattern-implicit-args: @@ -301,8 +301,8 @@ Controlling reversible-pattern implicit arguments .. flag:: Reversible Pattern Implicit - By default, |Coq| does not automatically set implicit the reversible-pattern - implicit arguments. You can turn this flag on to tell |Coq| to also infer + By default, Coq does not automatically set implicit the reversible-pattern + implicit arguments. You can turn this flag on to tell Coq to also infer reversible-pattern implicit argument. .. _controlling-insertion-implicit-args: |