diff options
| author | Lysxia | 2019-03-16 19:01:53 -0400 |
|---|---|---|
| committer | Lysxia | 2019-03-17 09:36:02 -0400 |
| commit | 211a241f81f80cfc17afc9f1f203a4a5805b8b4a (patch) | |
| tree | f1ae4849ae6d950b3d33a30f1d2732e64101d49a /doc/sphinx/language | |
| parent | 3b57b6c205f0ed1fac51fedf72cc8cf451bf2de7 (diff) | |
[Manual] Improve chapter Type classes, and add mention of Context under Variable
- More consistent code indentation
- Nest command variants properly
- Make `Context` explanation a bit less terse, with more links
- Typesetting bits, add some :cmd: links
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 02fb9d84ce..158a3f5ffc 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -639,6 +639,9 @@ has type :token:`type`. parametrized (the variable is *discharged*). Using the :cmd:`Variable` command out of any section is equivalent to using :cmd:`Local Parameter`. + See also :cmd:`Context`, a variant of :cmd:`Variable` where variables can be + made implicit and allowing :ref:`implicit-generalization`. + .. exn:: @ident already exists. :name: @ident already exists. (Variable) :undocumented: |