From 05276561ebff16d434b475b9e80586194619a832 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 29 Oct 2015 10:27:51 +0100
Subject: ENH: the concept of the 'algebraic universe' was added to the 'Global
 Index'.

---
 doc/refman/RefMan-cic.tex | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 702adc2326..7f9d4e5ecb 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -78,8 +78,9 @@ We shall make precise in the typing rules the constraints between the
 indexes. 
 
 \paragraph{Implementation issues}
-In practice, the {\Type} hierarchy is implemented using algebraic
-universes. An algebraic universe $u$ is either a variable (a qualified
+In practice, the {\Type} hierarchy is implemented using
+{\em algebraic universes}\index{algebraic universe}.
+An algebraic universe $u$ is either a variable (a qualified
 identifier with a number) or a successor of an algebraic universe (an
 expression $u+1$), or an upper bound of algebraic universes (an
 expression $max(u_1,...,u_n)$), or the base universe (the expression
-- 
cgit v1.2.3