diff options
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: |