diff options
| author | Emilio Jesus Gallego Arias | 2020-02-21 16:18:54 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-21 16:18:54 -0500 |
| commit | c45b7e41a1caa4d5ec4785c2bf323bdd11ad8d2e (patch) | |
| tree | 86d2847ee9b7c34c602fe41715afa171e41ffeba /doc/sphinx | |
| parent | 3f7eb03c82c9db9673cc8ae9c81c8f9132003751 (diff) | |
| parent | 779b8a105e3e06bde673c1abc4f918101c113fe2 (diff) | |
Merge PR #11261: Use implicit types for printing (granting wish #10366).
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index f0bbaed8f3..9686500a35 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2208,6 +2208,13 @@ or :g:`m` to the type :g:`nat` of natural numbers). Adds blocks of implicit types with different specifications. +.. flag:: Printing Use Implicit Types + + By default, the type of bound variables is not printed when + the variable name is associated to an implicit type which matches the + actual type of the variable. This feature can be deactivated by + turning this flag off. + .. _implicit-generalization: Implicit generalization |