diff options
Diffstat (limited to 'doc/refman/Universes.tex')
| -rw-r--r-- | doc/refman/Universes.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index ea3cca77e..a08cd1475 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -159,6 +159,7 @@ unification can have different unfolding behaviors on the same development with universe polymorphism switched on or off. \asection{Minimization} +\optindex{Universe Minimization ToSet} Universe polymorphism with cumulativity tends to generate many useless inclusion constraints in general. Typically at each application of a @@ -248,7 +249,7 @@ User-named universes are considered rigid for unification and are never minimized. \subsection{\tt Unset Strict Universe Declaration. - \optindex{StrictUniverseDeclaration} + \optindex{Strict Universe Declaration} \label{StrictUniverseDeclaration}} The command \texttt{Unset Strict Universe Declaration} allows one to |