From 0d580ce929060df98b7d566a40adc2e46c4a1d6c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 20 Jul 2017 13:33:09 +0200
Subject: [refman] Expand a little on global universes.

---
 doc/refman/Universes.tex | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 75fac9454a..a1a6a43918 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.
 
-- 
cgit v1.2.3