diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 12:56:11 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 12:56:11 +0100 |
| commit | 2c5e81e3bc6ec17d253aeedd1b2bf4ccd3b81933 (patch) | |
| tree | 1e8d3db28d8d19b575e9e555f6ce379960c842c1 /doc | |
| parent | d403b2200ef32afd1eb1087a1f0ef2e6b8bb93f6 (diff) | |
| parent | 17b620f8bdf47a744d24513dcaef720d9160d443 (diff) | |
Merge PR #890: Global universe declarations
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/Universes.tex | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 75fac9454..a1a6a4391 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -285,8 +285,10 @@ universes and explicitly instantiate polymorphic definitions. \label{UniverseCmd}} In the monorphic case, this command declares a new global universe named -{\ident}. It supports the polymorphic flag only in sections, meaning the -universe quantification will be discharged on each section definition +{\ident}, which can be referred to using its qualified name as +well. Global universe names live in a separate namespace. The command +supports the polymorphic flag only in sections, meaning the universe +quantification will be discharged on each section definition independently. One cannot mix polymorphic and monomorphic declarations in the same section. |