Index: doc/refrat/refrat.tex
===================================================================
--- doc/refrat/refrat.tex	(revision 32a1e5fd4bfb9f3c11a49cb264a4781656cd15ba)
+++ doc/refrat/refrat.tex	(revision 2fc0e5c4898b2a1a75d9696889cb23f22180b27b)
@@ -1,2 +1,4 @@
+% requires tex packages: texlive-base texlive-latex-base tex-common texlive-humanities texlive-latex-extra texlive-fonts-recommended
+
 \documentclass[openright,twoside]{report}
 \usepackage{fullpage,times}
@@ -55,4 +57,20 @@
 \def\c11{ISO/IEC C}% cannot have numbers in latex command name
 
+% replace/adjust characters that look bad in sanserif
+\makeatletter
+\lst@CCPutMacro
+\lst@ProcessOther{"2D}{\lst@ttfamily{-{}}{{\ttfamily\upshape -}}} % replace minus
+\lst@ProcessOther{"3C}{\lst@ttfamily{<}{\texttt{<}}} % replace less than
+\lst@ProcessOther{"3E}{\lst@ttfamily{<}{\texttt{>}}} % replace greater than
+\lst@ProcessOther{"5E}{$\sim$} % circumflex
+\lst@ProcessLetter{"5F}{\lst@ttfamily{\char95}{{\makebox[1.2ex][c]{\rule{1ex}{0.1ex}}}}} % replace underscore
+\lst@ProcessOther{"7E}{\raisebox{-.4ex}[1ex][0pt]{\textasciitilde}} % lower tilde
+\@empty\z@\@empty
+
+\newcommand{\Index}{\@ifstar\@sIndex\@Index}
+\newcommand{\@Index}[2][\@empty]{\lowercase{\def\temp{#2}}#2\ifx#1\@empty\index{\temp}\else\index{#1@{\protect#2}}\fi}
+\newcommand{\@sIndex}[2][\@empty]{#2\ifx#1\@empty\index{#2}\else\index{#1@{\protect#2}}\fi}
+\makeatother
+
 \lstdefinelanguage{CFA}[ANSI]{C}%
   {morekeywords={asm,_Atomic,catch,choose,_Complex,context,dtype,fallthru,forall,ftype,_Imaginary,lvalue,restrict,throw,try,type,},
@@ -71,4 +89,5 @@
 
 \setcounter{secnumdepth}{3}     % number subsubsections
+\setcounter{tocdepth}{3}		% subsubsections in table of contents
 \makeindex
 
@@ -142,12 +161,11 @@
 
 \CFA's scope rules differ from C's in one major respect: a declaration of an identifier may
-overload\index{overloading} outer declarations of lexically identical identifiers in the same name
-space\index{name spaces}, instead of hiding them. The outer declaration is hidden if the two
-declarations have compatible type\index{compatible type}, or if one declares an array type and the
-other declares a pointer type and the element type and pointed-at type are compatible, or if one has
-function type and the other is a pointer to a compatible function type, or if one declaration is a
-\lstinline$type$\use{type} or \lstinline$typedef$\use{typedef} declaration and the other is not.
-The outer declaration becomes visible\index{visible} when the scope of the inner declaration
-terminates.
+overload\index{overloading} outer declarations of lexically identical identifiers in the same
+\Index{name space}, instead of hiding them. The outer declaration is hidden if the two declarations
+have \Index{compatible type}, or if one declares an array type and the other declares a pointer type
+and the element type and pointed-at type are compatible, or if one has function type and the other
+is a pointer to a compatible function type, or if one declaration is a \lstinline$type$\use{type} or
+\lstinline$typedef$\use{typedef} declaration and the other is not.  The outer declaration becomes
+\Index{visible} when the scope of the inner declaration terminates.
 \begin{rationale}
 Hence, a \CFA program can declare an \lstinline$int v$ and a \lstinline$float v$ in the same
@@ -156,16 +174,16 @@
 
 
-\subsection{Linkage of identifiers}\index{linkage}
-
-\CFA's linkage rules differ from C's in only one respect: instances of a particular identifier
-with external or internal linkage do not necessarily denote the same object or function. Instead,
-in the set of translation units and libraries that constitutes an entire program, any two instances
-of a particular identifier with external linkage\index{external linkage} denote the same object or
-function if they have compatible types\index{compatible type}, or if one declares an array type and
-the other declares a pointer type and the element type and pointed-at type are compatible, or if one
-has function type and the other is a pointer to a compatible function type. Within one translation
-unit, each instance of an identifier with internal linkage\index{internal linkage} denotes the same
-object or function in the same circumstances. Identifiers with no linkage\index{no linkage} always
-denote unique entities.
+\subsection{Linkage of identifiers}
+\index{linkage}
+
+\CFA's linkage rules differ from C's in only one respect: instances of a particular identifier with
+external or internal linkage do not necessarily denote the same object or function. Instead, in the
+set of translation units and libraries that constitutes an entire program, any two instances of a
+particular identifier with \Index{external linkage} denote the same object or function if they have
+\Index{compatible type}s, or if one declares an array type and the other declares a pointer type and
+the element type and pointed-at type are compatible, or if one has function type and the other is a
+pointer to a compatible function type. Within one translation unit, each instance of an identifier
+with \Index{internal linkage} denotes the same object or function in the same circumstances.
+Identifiers with \Index{no linkage} always denote unique entities.
 \begin{rationale}
 A \CFA program can declare an \lstinline$extern int v$ and an \lstinline$extern float v$; a C
@@ -175,6 +193,6 @@
 \section{Conversions}
 \CFA defines situations where values of one type are automatically converted to another type.
-These conversions are called \define{implicit conversions}. The programmer can request
-\define{explicit conversions} using cast expressions.
+These conversions are called \define{implicit conversion}s. The programmer can request
+\define{explicit conversion}s using cast expressions.
 
 
@@ -184,11 +202,11 @@
 
 \subsubsection{Safe arithmetic conversions}
-In C, a pattern of conversions known as the \define{usual arithmetic conversions} is used with most
+In C, a pattern of conversions known as the \define{usual arithmetic conversion}s is used with most
 binary arithmetic operators to convert the operands to a common type and determine the type of the
 operator's result. In \CFA, these conversions play a role in overload resolution, and
-collectively are called the \define{safe arithmetic conversions}.
+collectively are called the \define{safe arithmetic conversion}s.
 
 Let \(int_r\) and \(unsigned_r\) be the signed and unsigned integer types with integer conversion
-rank\index{integer conversion rank} \index{rank|see{integer conversion rank}} $r$. Let
+rank\index{integer conversion rank}\index{rank|see{integer conversion rank}} $r$. Let
 \(unsigned_{mr}\) be the unsigned integer type with maximal rank.
 
@@ -196,5 +214,5 @@
 \begin{itemize}
 \item
-The integer promotions\index{integer promotions}.
+The \Index{integer promotion}s.
 
 \item
@@ -234,7 +252,6 @@
 
 \begin{rationale}
-Note that {\c11} does not include conversion from real types\index{real type} to complex
-types\index{complex type} in the usual arithmetic conversions, and \CFA does not include them as
-safe conversions.
+Note that {\c11} does not include conversion from \Index{real type}s to \Index{complex type}s in the
+usual arithmetic conversions, and \CFA does not include them as safe conversions.
 \end{rationale}
 
@@ -248,7 +265,7 @@
 
 If an expression's type is a pointer to a structure or union type that has a member that is an
-anonymous structure\index{anonymous structure} or an anonymous union\index{anonymous union}, it can
-be implicitly converted\index{implicit conversions} to a pointer to the anonymous structure's or
-anonymous union's type. The result of the conversion is a pointer to the member.
+\Index{anonymous structure} or an \Index{anonymous union}, it can be implicitly
+converted\index{implicit conversion} to a pointer to the anonymous structure's or anonymous union's
+type. The result of the conversion is a pointer to the member.
 
 \examples
@@ -273,14 +290,13 @@
 
 \subsubsection{Specialization}
-A function or value whose type is polymorphic may be implicitly converted to one whose type is less
-polymorphic\index{less polymorphic} by binding values to one or more of its inferred
-parameters\index{inferred parameter}. Any value that is legal for the inferred parameter may be
-used, including other inferred parameters.
-
-If, after the inferred parameter binding, an assertion parameter\index{assertion parameters} has no
-inferred parameters in its type, then an object or function must be visible at the point of the
-specialization that has the same identifier as the assertion parameter and has a type that is
-compatible\index{compatible type} with or can be specialized to the type of the assertion parameter.
-The assertion parameter is bound to that object or function.
+A function or value whose type is polymorphic may be implicitly converted to one whose type is
+\Index{less polymorphic} by binding values to one or more of its \Index{inferred parameter}. Any
+value that is legal for the inferred parameter may be used, including other inferred parameters.
+
+If, after the inferred parameter binding, an \Index{assertion parameter} has no inferred parameters
+in its type, then an object or function must be visible at the point of the specialization that has
+the same identifier as the assertion parameter and has a type that is compatible\index{compatible
+  type} with or can be specialized to the type of the assertion parameter.  The assertion parameter
+is bound to that object or function.
 
 The type of the specialization is the type of the original with the bound inferred parameters and
@@ -325,12 +341,11 @@
 \item
 from a pointer to a structure or union type to a pointer to the type of a member of the structure or
-union that is an anonymous structure\index{anonymous structure} or an anonymous
-union\index{anonymous union};
-\item
-within the scope of an initialized type declaration\index{type declaration}, conversions between a
-type and its implementation or between a pointer to a type and a pointer to its implementation.
+union that is an \Index{anonymous structure} or an \Index{anonymous union};
+\item
+within the scope of an initialized \Index{type declaration}, conversions between a type and its
+implementation or between a pointer to a type and a pointer to its implementation.
 \end{itemize}
 
-Conversions that are not safe conversions are \define{unsafe conversions}.
+Conversions that are not safe conversions are \define{unsafe conversion}s.
 \begin{rationale}
 As in C, there is an implicit conversion from \lstinline$void *$ to any pointer type. This is
@@ -343,6 +358,6 @@
 \subsection{Conversion cost}
 
-The \define{conversion cost} of a safe\index{safe conversions}
-conversion\footnote{Unsafe\index{unsafe conversions} conversions do not have defined conversion
+The \define{conversion cost} of a safe\index{safe conversion}
+conversion\footnote{Unsafe\index{unsafe conversion} conversions do not have defined conversion
 costs.} is a measure of how desirable or undesirable it is. It is defined as follows.
 \begin{itemize}
@@ -395,9 +410,9 @@
 \subsection{Identifiers}
 
-\CFA allows operator overloading\index{overloading} by associating operators with special
-function identifiers. Furthermore, the constants ``\lstinline$0$'' and ``\lstinline$1$'' have
-special status for many of C's data types (and for many programmer-defined data types as well), so
-\CFA treats them as overloadable identifiers. Programmers can use these identifiers to declare
-functions and objects that implement operators and constants for their own types.
+\CFA allows operator \Index{overloading} by associating operators with special function
+identifiers. Furthermore, the constants ``\lstinline$0$'' and ``\lstinline$1$'' have special status
+for many of C's data types (and for many programmer-defined data types as well), so \CFA treats them
+as overloadable identifiers. Programmers can use these identifiers to declare functions and objects
+that implement operators and constants for their own types.
 
 
@@ -561,7 +576,8 @@
 
 \section{Expressions}
+
 \CFA allows operators and identifiers to be overloaded. Hence, each expression can have a number
-of \define{interpretations}, each of which has a different type. The interpretations that are
-potentially executable are called \define{valid interpretations}. The set of interpretations
+of \define{interpretation}s, each of which has a different type. The interpretations that are
+potentially executable are called \define{valid interpretation}s. The set of interpretations
 depends on the kind of expression and on the interpretations of the subexpressions that it contains.
 The rules for determining the valid interpretations of an expression are discussed below for each
@@ -575,11 +591,11 @@
 
 The \define{best valid interpretations} are the valid interpretations that use the fewest
-unsafe\index{unsafe conversions} conversions. Of these, the best are those where the functions and
+unsafe\index{unsafe conversion} conversions. Of these, the best are those where the functions and
 objects involved are the least polymorphic\index{less polymorphic}. Of these, the best have the
-lowest total conversion cost\index{conversion cost}, including all implicit conversions in the
-argument expressions. Of these, the best have the highest total conversion cost for the implicit
-conversions (if any) applied to the argument expressions. If there is no single best valid
-interpretation, or if the best valid interpretation is ambiguous, then the resulting interpretation
-is ambiguous\index{ambiguous interpretation}.
+lowest total \Index{conversion cost}, including all implicit conversions in the argument
+expressions. Of these, the best have the highest total conversion cost for the implicit conversions
+(if any) applied to the argument expressions. If there is no single best valid interpretation, or if
+the best valid interpretation is ambiguous, then the resulting interpretation is
+ambiguous\index{ambiguous interpretation}.
 
 \begin{rationale}
@@ -595,9 +611,9 @@
 The ``least polymorphic'' rule reduces the number of polymorphic function calls, since such
 functions are presumably more expensive than monomorphic functions and since the more specific
-function is presumably more appropriate. It also gives preference to monomorphic values (such as
-the \lstinline$int$ \lstinline$0$) over polymorphic values (such as the null pointer
-\lstinline$0$)\use{0}\index{null pointer}. However, interpretations that call polymorphic functions
-are preferred to interpretations that perform unsafe conversions, because those conversions
-potentially lose accuracy or violate strong typing.
+function is presumably more appropriate. It also gives preference to monomorphic values (such as the
+\lstinline$int$ \lstinline$0$) over polymorphic values (such as the \Index{null pointer}
+\lstinline$0$\use{0}). However, interpretations that call polymorphic functions are preferred to
+interpretations that perform unsafe conversions, because those conversions potentially lose accuracy
+or violate strong typing.
 
 There are two notable differences between \CFA's overload resolution rules and the rules for
@@ -614,7 +630,7 @@
 by \define{rewrite rules}. Each operator has a set of predefined functions that overload its
 identifier. Overload resolution determines which member of the set is executed in a given
-expression. The functions have internal linkage\index{internal linkage} and are implicitly declared
-with file scope\index{file scope}. The predefined functions and rewrite rules are discussed below
-for each of these operators.
+expression. The functions have \Index{internal linkage} and are implicitly declared with \Index{file
+scope}. The predefined functions and rewrite rules are discussed below for each of these
+operators.
 \begin{rationale}
 Predefined functions and constants have internal linkage because that simplifies optimization in
@@ -629,8 +645,8 @@
 of its subexpressions, this chapter can be taken as describing an overload resolution algorithm that
 uses one bottom-up pass over an expression tree. Such an algorithm was first described (for Ada) by
-Baker \cite{Bak:overload}. It is extended here to handle polymorphic functions and arithmetic
-conversions. The overload resolution rules and the predefined functions have been chosen so that,
-in programs that do not introduce overloaded declarations, expressions will have the same meaning in
-C and in \CFA.
+Baker~\cite{Bak:overload}. It is extended here to handle polymorphic functions and arithmetic
+conversions. The overload resolution rules and the predefined functions have been chosen so that, in
+programs that do not introduce overloaded declarations, expressions will have the same meaning in C
+and in \CFA.
 \end{rationale}
 
@@ -641,5 +657,7 @@
 \end{rationale}
 
+
 \subsection{Primary expressions}
+
 \begin{syntax}
 \lhs{primary-expression}
@@ -660,6 +678,6 @@
 
 \semantics
-The valid interpretations\index{valid interpretations} of an \nonterm{identifier} are given by the
-visible\index{visible} declarations of the identifier.
+The \Index{valid interpretation} of an \nonterm{identifier} are given by the visible\index{visible}
+declarations of the identifier.
 
 A \nonterm{constant} or \nonterm{string-literal} has one valid interpretation, which has the type
@@ -702,5 +720,7 @@
 \end{rationale}
 
+
 \subsubsection{Generic selection}
+
 \constraints The best interpretation of the controlling expression shall be
 unambiguous\index{ambiguous interpretation}, and shall have type compatible with at most one of the
@@ -742,5 +762,7 @@
 \end{lstlisting}
 
+
 \subsubsection{Array subscripting}
+
 \begin{lstlisting}
 forall( type T ) lvalue T ?[?]( T *, ptrdiff_t );@\use{ptrdiff_t}@
@@ -794,8 +816,8 @@
 
 Each combination of function designators and argument interpretations is considered. For those
-interpretations of the \nonterm{postfix-expression} that are monomorphic\index{monomorphic function}
-function designators, the combination has a valid interpretation\index{valid interpretations} if the
-function designator accepts the number of arguments given, and each argument interpretation matches
-the corresponding explicit parameter:
+interpretations of the \nonterm{postfix-expression} that are \Index{monomorphic function}
+designators, the combination has a \Index{valid interpretation} if the function designator accepts
+the number of arguments given, and each argument interpretation matches the corresponding explicit
+parameter:
 \begin{itemize}
 \item
@@ -805,23 +827,22 @@
 \item
 if the function designator's type does not include a prototype or if the argument corresponds to
-``\lstinline$...$'' in a prototype, a default argument promotion\index{default argument promotions}
-is applied to it.
+``\lstinline$...$'' in a prototype, a \Index{default argument promotion} is applied to it.
 \end{itemize}
 The type of the valid interpretation is the return type of the function designator.
 
 For those combinations where the interpretation of the \nonterm{postfix-expression} is a
-polymorphic\index{polymorphic function} function designator and the function designator accepts the
-number of arguments given, there shall be at least one set of \define{implicit arguments} for the
-implicit parameters such that
+\Index{polymorphic function} designator and the function designator accepts the number of arguments
+given, there shall be at least one set of \define{implicit argument}s for the implicit parameters
+such that
 \begin{itemize}
 \item
-If the declaration of the implicit parameter uses type-class\index{type-class}
-\lstinline$type$\use{type}, the implicit argument must be an object type; if it uses
-\lstinline$dtype$, the implicit argument must be an object type or an incomplete type; and if it
-uses \lstinline$ftype$, the implicit argument must be a function type.
+If the declaration of the implicit parameter uses \Index{type-class} \lstinline$type$\use{type}, the
+implicit argument must be an object type; if it uses \lstinline$dtype$, the implicit argument must
+be an object type or an incomplete type; and if it uses \lstinline$ftype$, the implicit argument
+must be a function type.
 
 \item
 if an explicit parameter's type uses any implicit parameters, then the corresponding explicit
-argument must have a type that is (or can be safely converted\index{safe conversions} to) the type
+argument must have a type that is (or can be safely converted\index{safe conversion} to) the type
 produced by substituting the implicit arguments for the implicit parameters in the explicit
 parameter type.
@@ -832,7 +853,7 @@
 
 \item
-for each assertion parameter\index{assertion parameters} in the function designator's type, there
-must be an object or function with the same identifier that is visible at the call site and whose
-type is compatible with or can be specialized to the type of the assertion declaration.
+for each \Index{assertion parameter} in the function designator's type, there must be an object or
+function with the same identifier that is visible at the call site and whose type is compatible with
+or can be specialized to the type of the assertion declaration.
 \end{itemize}
 There is a valid interpretation for each such set of implicit parameters. The type of each valid
@@ -848,6 +869,6 @@
 Every set of valid interpretations that have mutually compatible\index{compatible type} result types
 also produces an interpretation of the function call expression. The type of the interpretation is
-the composite\index{composite type} type of the types of the valid interpretations, and the value of
-the interpretation is that of the best valid interpretation\index{best valid interpretations}.
+the \Index{composite type} of the types of the valid interpretations, and the value of the
+interpretation is that of the \Index{best valid interpretation}.
 \begin{rationale}
 One desirable property of a polymorphic programming language is \define{generalizability}: the
@@ -858,6 +879,6 @@
 
 \CFA\index{deficiencies!generalizability} does not fully possess this property, because
-unsafe\index{unsafe conversions} conversions are not done when arguments are passed to polymorphic
-parameters. Consider
+\Index{unsafe conversion} are not done when arguments are passed to polymorphic parameters.
+Consider
 \begin{lstlisting}
 float g( float, float );
@@ -960,9 +981,9 @@
 r( 0 );
 \end{lstlisting}
-The \lstinline$int 0$ could be passed to (8), or the \lstinline$(void *)$
-specialization\index{specialization} of the null pointer\index{null pointer} \lstinline$0$\use{0}
-could be passed to (9). The former is chosen because the \lstinline$int$ \lstinline$0$ is less
-polymorphic\index{less polymorphic}. For the same reason, \lstinline$int$ \lstinline$0$ is passed
-to \lstinline$r()$, even though it has \emph{no} declared parameter types.
+The \lstinline$int 0$ could be passed to (8), or the \lstinline$(void *)$ \Index{specialization} of
+the null pointer\index{null pointer} \lstinline$0$\use{0} could be passed to (9). The former is
+chosen because the \lstinline$int$ \lstinline$0$ is \Index{less polymorphic}. For
+the same reason, \lstinline$int$ \lstinline$0$ is passed to \lstinline$r()$, even though it has
+\emph{no} declared parameter types.
 
 
@@ -972,9 +993,9 @@
 least one interpretation of \lstinline$s$ whose type is a structure type or union type containing a
 member named \lstinline$m$. If two or more interpretations of \lstinline$s$ have members named
-\lstinline$m$ with mutually compatible types, then the expression has an ambiguous
-interpretation\index{ambiguous interpretation} whose type is the composite type of the types of the
-members. If an interpretation of \lstinline$s$ has a member \lstinline$m$ whose type is not
-compatible with any other \lstinline$s$'s \lstinline$m$, then the expression has an interpretation
-with the member's type. The expression has no other interpretations.
+\lstinline$m$ with mutually compatible types, then the expression has an \Index{ambiguous
+interpretation} whose type is the composite type of the types of the members. If an interpretation
+of \lstinline$s$ has a member \lstinline$m$ whose type is not compatible with any other
+\lstinline$s$'s \lstinline$m$, then the expression has an interpretation with the member's type. The
+expression has no other interpretations.
 
 The expression ``\lstinline$p->m$'' has the same interpretations as the expression
@@ -1147,5 +1168,5 @@
 \begin{lstlisting}
 X ?++( volatile X * ), ?++( _Atomic volatile X * ),
- ?--( volatile X * ), ?--( _Atomic volatile X * );
+  ?--( volatile X * ), ?--( _Atomic volatile X * );
 \end{lstlisting}
 For every complete enumerated type \lstinline$E$ there exist
@@ -1153,5 +1174,5 @@
 \begin{lstlisting}
 E ?++( volatile E * ), ?++( _Atomic volatile E * ),
- ?--( volatile E * ), ?--( _Atomic volatile E * );
+  ?--( volatile E * ), ?--( _Atomic volatile E * );
 \end{lstlisting}
 
@@ -1174,7 +1195,7 @@
 First, each interpretation of the operand of an increment or decrement expression is considered
 separately. For each interpretation that is a bit-field or is declared with the
-\lstinline$register$\index{register@{\lstinline$register$}} storage-class
-specifier\index{storage-class specifier}, the expression has one valid interpretation, with the type
-of the operand, and the expression is ambiguous if the operand is.
+\lstinline$register$\index{register@{\lstinline$register$}} \index{Itorage-class specifier}, the
+expression has one valid interpretation, with the type of the operand, and the expression is
+ambiguous if the operand is.
 
 For the remaining interpretations, the expression is rewritten, and the interpretations of the
@@ -1523,5 +1544,5 @@
 \constraints
 The operand of the unary ``\lstinline$&$'' operator shall have exactly one
-interpretation\index{ambiguous interpretation}\index{interpretations}, which shall be unambiguous.
+\Index{interpretation}\index{ambiguous interpretation}, which shall be unambiguous.
 
 \semantics
@@ -1596,6 +1617,6 @@
 forall( ftype FT ) int !?( FT * );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with integer conversion rank \index{integer conversion
-rank}greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -1660,5 +1681,5 @@
 
 
-\subsubsection{The {\tt sizeof} and {\tt \_Alignof} operators}
+\subsubsection{The \lstinline$sizeof$ and \lstinline$_Alignof$ operators}
 
 \constraints
@@ -1667,5 +1688,5 @@
 
 When the \lstinline$sizeof$\use{sizeof} operator is applied to an expression, the expression shall
-have exactly one interpretation\index{ambiguous interpretation}\index{interpretations}, which shall
+have exactly one \Index{interpretation}\index{ambiguous interpretation}, which shall
 be unambiguous. \semantics A \lstinline$sizeof$ or \lstinline$_Alignof$ expression has one
 interpretation, of type \lstinline$size_t$.
@@ -1697,5 +1718,7 @@
 \end{rationale}
 
+
 \subsection{Cast operators}
+
 \begin{syntax}
 \lhs{cast-expression}
@@ -1710,11 +1733,11 @@
 \semantics
 
-In a cast expression\index{cast expression} ``\lstinline$($\nonterm{type-name}\lstinline$)e$'', if
-\nonterm{type-name} is the type of an interpretation of \lstinline$e$, then that interpretation is the
-only interpretation of the cast expression; otherwise, \lstinline$e$ shall have some interpretation that
-can be converted to \nonterm{type-name}, and the interpretation of the cast expression is the cast
-of the interpretation that can be converted at the lowest cost. The cast expression's interpretation
-is ambiguous\index{ambiguous interpretation} if more than one interpretation can be converted at the
-lowest cost or if the selected interpretation is ambiguous.
+In a \Index{cast expression} ``\lstinline$($\nonterm{type-name}\lstinline$)e$'', if
+\nonterm{type-name} is the type of an interpretation of \lstinline$e$, then that interpretation is
+the only interpretation of the cast expression; otherwise, \lstinline$e$ shall have some
+interpretation that can be converted to \nonterm{type-name}, and the interpretation of the cast
+expression is the cast of the interpretation that can be converted at the lowest cost. The cast
+expression's interpretation is ambiguous\index{ambiguous interpretation} if more than one
+interpretation can be converted at the lowest cost or if the selected interpretation is ambiguous.
 
 \begin{rationale}
@@ -1723,5 +1746,7 @@
 \end{rationale}
 
+
 \subsection{Multiplicative operators}
+
 \begin{syntax}
 \lhs{multiplicative-expression}
@@ -1783,6 +1808,6 @@
 	?/?( _Complex long double, _Complex long double );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with integer conversion rank \index{integer conversion
-rank}greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -1791,8 +1816,7 @@
 
 \begin{rationale}
-{\c11} does not include conversions from the real types\index{real type} to complex
-types\index{complex type} in the usual arithmetic conversions\index{usual arithmetic conversions}.
-Instead it specifies conversion of the result of binary operations on arguments from mixed type
-domains. \CFA's predefined operators match that pattern.
+{\c11} does not include conversions from the \Index{real type}s to \Index{complex type}s in the
+\Index{usual arithmetic conversion}s.  Instead it specifies conversion of the result of binary
+operations on arguments from mixed type domains. \CFA's predefined operators match that pattern.
 \end{rationale}
 
@@ -1829,10 +1853,9 @@
 
 \begin{rationale}
-{\c11} defines most arithmetic operations to apply an integer promotion\index{integer promotions} to
-any argument that belongs to a type that has an integer conversion rank\index{integer conversion
- rank} less than that of \lstinline$int$.If \lstinline$s$ is a \lstinline$short int$,
-``\lstinline$s *s$'' does not have type \lstinline$short int$; it is treated as
-``\lstinline$( (int)s ) * ( (int)s )$'', and has type \lstinline$int$. \CFA matches that pattern;
-it does not predefine ``\lstinline$short ?*?( short, short )$''.
+{\c11} defines most arithmetic operations to apply an \Index{integer promotion} to any argument that
+belongs to a type that has an \Index{integer conversion rank} less than that of \lstinline$int$.If
+\lstinline$s$ is a \lstinline$short int$, ``\lstinline$s *s$'' does not have type \lstinline$short int$;
+it is treated as ``\lstinline$( (int)s ) * ( (int)s )$'', and has type \lstinline$int$. \CFA matches
+that pattern; it does not predefine ``\lstinline$short ?*?( short, short )$''.
 
 These ``missing'' operators limit polymorphism. Consider
@@ -1986,7 +2009,6 @@
 	* ?-?( _Atomic const restrict volatile T *, _Atomic const restrict volatile T * );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with integer conversion rank
-\index{integer conversion rank}greater than the rank of \lstinline$int$ there
-exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -2039,6 +2061,6 @@
 	 ?>>?( long long unsigned int, int);
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with integer conversion rank \index{integer conversion
- rank}greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -2048,5 +2070,5 @@
 \begin{rationale}
 The bitwise shift operators break the usual pattern: they do not convert both operands to a common
-type. The right operand only undergoes integer promotion\index{integer promotion}.
+type. The right operand only undergoes \Index{integer promotion}.
 \end{rationale}
 
@@ -2123,6 +2145,6 @@
 	?>=?( _Atomic const restrict volatile DT *, _Atomic const restrict volatile DT * );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with integer conversion rank \index{integer conversion
- rank}greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -2226,6 +2248,6 @@
 	?!=?( forall( ftype FT2) FT2*, forall( ftype FT3) FT3 * );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with integer conversion rank \index{integer conversion
- rank}greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -2237,7 +2259,7 @@
 The polymorphic equality operations come in three styles: comparisons between pointers of compatible
 types, between pointers to \lstinline$void$ and pointers to object types or incomplete types, and
-between the null pointer constant\index{null pointer} and pointers to any type. In the last case, a
-special constraint rule for null pointer constant operands has been replaced by a consequence of the
-\CFA type system.
+between the \Index{null pointer} constant and pointers to any type. In the last case, a special
+constraint rule for null pointer constant operands has been replaced by a consequence of the \CFA
+type system.
 \end{rationale}
 
@@ -2278,6 +2300,6 @@
 long long unsigned int ?&?( long long unsigned int, long long unsigned int );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with integer conversion rank \index{integer conversion
-rank}greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -2311,6 +2333,6 @@
 long long unsigned int ?^?( long long unsigned int, long long unsigned int );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with integer conversion rank \index{integer conversion
- rank}greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -2344,6 +2366,6 @@
 long long unsigned int ?|?( long long unsigned int, long long unsigned int );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with integer conversion rank \index{integer conversion
-rank}greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -2502,7 +2524,7 @@
 
 \begin{rationale}
-The object of the above is to apply the usual arithmetic conversions\index{usual arithmetic
-conversions} when the second and third operands have arithmetic type, and to combine the
-qualifiers of the second and third operands if they are pointers.
+The object of the above is to apply the \Index{usual arithmetic conversion}s when the second and
+third operands have arithmetic type, and to combine the qualifiers of the second and third operands
+if they are pointers.
 \end{rationale}
 
@@ -3172,7 +3194,7 @@
 
 \constraints
-If an identifier has no linkage\index{no linkage}, there shall be no more than one declaration of
-the identifier ( in a declarator or type specifier ) with compatible types in the same scope and in
-the same name space, except that:
+If an identifier has \Index{no linkage}, there shall be no more than one declaration of the
+identifier ( in a declarator or type specifier ) with compatible types in the same scope and in the
+same name space, except that:
 \begin{itemize}
 \item
@@ -3276,5 +3298,5 @@
 \semantics
 The \nonterm{type-parameter-list}s and assertions of the \nonterm{forall-specifier}s declare type
-identifiers, function and object identifiers with no linkage\index{no linkage}.
+identifiers, function and object identifiers with \Index{no linkage}.
 
 If, in the declaration ``\lstinline$T D1$'', \lstinline$T$ contains \nonterm{forall-specifier}s and
@@ -3284,10 +3306,10 @@
 \end{lstlisting}
 then a type identifier declared by one of the \nonterm{forall-specifier}s is an \define{inferred
- parameter} of the function declarator if and only if it is not an inferred parameter of a function
+parameter} of the function declarator if and only if it is not an inferred parameter of a function
 declarator in \lstinline$D$, and it is used in the type of a parameter in the following
 \nonterm{type-parameter-list} or it and an inferred parameter are used as arguments of a
-specification\index{specification} in one of the \nonterm{forall-specifier}s. The identifiers
-declared by assertions that use an inferred parameter of a function declarator are assertion
-parameters\index{assertion parameters} of that function declarator.
+\Index{specification} in one of the \nonterm{forall-specifier}s. The identifiers declared by
+assertions that use an inferred parameter of a function declarator are \Index{assertion parameter}s
+of that function declarator.
 \begin{rationale}
 Since every inferred parameter is used by some parameter, inference can be understood as a single
@@ -3312,5 +3334,5 @@
 
 If a function declarator is part of a function definition, its inferred parameters and assertion
-parameters have block scope\index{block scope}; otherwise, identifiers declared by assertions have a
+parameters have \Index{block scope}; otherwise, identifiers declared by assertions have a
 \define{declaration scope}, which terminates at the end of the \nonterm{declaration}.
 
@@ -3326,7 +3348,7 @@
 and $g$ in their order of occurance in the function types' \nonterm{parameter-type-list}s. Let $f'$
 be $f$ with every occurrence of $f_i$ replaced by $g_i$, for all $i$. Then $f$ and $g$ are
-compatible types\index{compatible type} if $f'$'s and $g$'s return types and parameter lists are
-compatible, and if for every assertion parameter of $f'$ there is an assertion parameter in $g$ with
-the same identifier and compatible type, and vice versa.
+\Index{compatible type}s if $f'$'s and $g$'s return types and parameter lists are compatible, and if
+for every assertion parameter of $f'$ there is an assertion parameter in $g$ with the same
+identifier and compatible type, and vice versa.
 
 \examples
@@ -3438,5 +3460,5 @@
 \lstinline$lvalue$ may be used to qualify the return type of a function type. Let \lstinline$T$ be
 an unqualified version of a type; then the result of calling a function with return type
-\lstinline$lvalue T$ is a modifiable lvalue\index{modifiable lvalue} of type \lstinline$T$.
+\lstinline$lvalue T$ is a \Index{modifiable lvalue} of type \lstinline$T$.
 \lstinline$const$\use{const} and \lstinline$volatile$\use{volatile} qualifiers may also be added to
 indicate that the function result is a constant or volatile lvalue.
@@ -3446,6 +3468,6 @@
 \end{rationale}
 
-An {lvalue}-qualified type may be used in a cast expression\index{cast expression} if the operand is
-an lvalue; the result of the expression is an lvalue.
+An {lvalue}-qualified type may be used in a \Index{cast expression} if the operand is an lvalue; the
+result of the expression is an lvalue.
 
 \begin{rationale}
@@ -3490,7 +3512,7 @@
 
 \item
-References to const-qualified\index{const-qualified} types can be used instead of value parameters.
-Given the {\CC} function call ``\lstinline$fiddle( a_thing )$'', where the type of
-\lstinline$a_thing$ is \lstinline$Thing$, the type of \lstinline$fiddle$ could be either of
+References to \Index{const-qualified} types can be used instead of value parameters.  Given the
+{\CC} function call ``\lstinline$fiddle( a_thing )$'', where the type of \lstinline$a_thing$ is
+\lstinline$Thing$, the type of \lstinline$fiddle$ could be either of
 \begin{lstlisting}
 void fiddle( Thing );
@@ -3525,5 +3547,5 @@
 object being initialized. An expression used in an \nonterm{initializer-list} is treated as being
 cast to the type of the aggregate member that it initializes. In either case the cast must have a
-single unambiguous interpretation\index{interpretations}.
+single unambiguous \Index{interpretation}.
 
 
@@ -3547,6 +3569,5 @@
 \begin{rationale}
 The declarations allowed in a specification are much the same as those allowed in a structure,
-except that bit fields are not allowed, and incomplete types\index{incomplete types} and function
-types are allowed.
+except that bit fields are not allowed, and \Index{incomplete type}s and function types are allowed.
 \end{rationale}
 
@@ -3563,4 +3584,5 @@
 
 \subsubsection{Assertions}
+
 \begin{syntax}
 \lhs{assertion-list}
@@ -3580,7 +3602,7 @@
 each \nonterm{type-parameter} in that specification's \nonterm{spec-parameter-list}. If the
 \nonterm{type-parameter} uses type-class \lstinline$type$\use{type}, the argument shall be the type
-name of an object type\index{object types}; if it uses \lstinline$dtype$, the argument shall be the
-type name of an object type or an incomplete type\index{incomplete types}; and if it uses
-\lstinline$ftype$, the argument shall be the type name of a function type\index{function types}.
+name of an \Index{object type}; if it uses \lstinline$dtype$, the argument shall be the type name of
+an object type or an \Index{incomplete type}; and if it uses \lstinline$ftype$, the argument shall
+be the type name of a \Index{function type}.
 
 \semantics
@@ -3595,5 +3617,5 @@
 combining the declarations produced by each assertion. If the collection contains two declarations
 that declare the same identifier and have compatible types, they are combined into one declaration
-with the composite type\index{composite type} constructed from the two types.
+with the \Index{composite type} constructed from the two types.
 
 \examples
@@ -3630,5 +3652,7 @@
 \end{lstlisting}
 
+
 \subsection{Type declarations}
+
 \begin{syntax}
 \lhs{type-parameter-list}
@@ -3656,28 +3680,26 @@
 
 \semantics
-A \nonterm{type-parameter} or a \nonterm{type-declarator} declares an identifier to be a type
-name\index{type names} for a type incompatible with all other types.
-
-An identifier declared by a \nonterm{type-parameter} has no linkage\index{no linkage}. Identifiers
-declared with type-class \lstinline$type$\use{type} are object types\index{object types}; those
-declared with type-class \lstinline$dtype$\use{dtype} are incomplete types\index{incomplete types};
-and those declared with type-class \lstinline$ftype$\use{ftype} are function types\index{function
- types}. The identifier has block scope\index{block scope} that terminates at the end of the
-\nonterm{spec-declaration-list} or polymorphic function that contains the \nonterm{type-parameter}.
-
-A \nonterm{type-declarator} with an initializer\index{initializer} is a \define{type definition}.
-The declared identifier is an incomplete type\index{incomplete types} within the initializer, and an
-object type\index{object types} after the end of the initializer. The type in the initializer is
-called the \define{implementation type}. Within the scope of the declaration, implicit
-conversions\index{implicit conversions} can be performed between the defined type and the
-implementation type, and between pointers to the defined type and pointers to the implementation
-type.
-
-A type declaration without an initializer\index{initializer} and without a storage-class
-specifier\index{storage-class specifiers} or with storage-class specifier
-\lstinline$static$\use{static} defines an incomplete type\index{incomplete types}. If a translation
-unit\index{translation unit} or block \index{block} contains one or more such declarations for an
-identifier, it must contain exactly one definition of the identifier ( but not in an enclosed block,
-which would define a new type known only within that block).
+A \nonterm{type-parameter} or a \nonterm{type-declarator} declares an identifier to be a \Index{type
+name} for a type incompatible with all other types.
+
+An identifier declared by a \nonterm{type-parameter} has \Index{no linkage}. Identifiers declared
+with type-class \lstinline$type$\use{type} are \Index{object type}s; those declared with type-class
+\lstinline$dtype$\use{dtype} are \Index{incomplete type}s; and those declared with type-class
+\lstinline$ftype$\use{ftype} are \Index{function type}s. The identifier has \Index{block scope} that
+terminates at the end of the \nonterm{spec-declaration-list} or polymorphic function that contains
+the \nonterm{type-parameter}.
+
+A \nonterm{type-declarator} with an \Index{initializer} is a \define{type definition}.  The declared
+identifier is an \Index{incomplete type} within the initializer, and an \Index{object type} after
+the end of the initializer. The type in the initializer is called the \define{implementation
+  type}. Within the scope of the declaration, \Index{implicit conversion}s can be performed between
+the defined type and the implementation type, and between pointers to the defined type and pointers
+to the implementation type.
+
+A type declaration without an \Index{initializer} and without a \Index{storage-class specifier} or
+with storage-class specifier \lstinline$static$\use{static} defines an \Index{incomplete type}. If a
+\Index{translation unit} or \Index{block} contains one or more such declarations for an identifier,
+it must contain exactly one definition of the identifier ( but not in an enclosed block, which would
+define a new type known only within that block).
 \begin{rationale}
 Incomplete type declarations allow compact mutually-recursive types.
@@ -3698,10 +3720,10 @@
 \end{rationale}
 
-A type declaration without an initializer and with storage-class specifier \index{storage-class
- specifiers} \lstinline$extern$\use{extern} is an \define{opaque type declaration}. Opaque types
-are object types\index{object types}. An opaque type is not a \nonterm{constant-expression};
-neither is a structure or union that has a member whose type is not a \nonterm{constant-expression}.
-Every other object type\index{object types} is a \nonterm{constant-expression}. Objects with static
-storage duration shall be declared with a type that is a \nonterm{constant-expression}.
+A type declaration without an initializer and with \Index{storage-class specifier}
+\lstinline$extern$\use{extern} is an \define{opaque type declaration}. Opaque types are
+\Index{object type}s. An opaque type is not a \nonterm{constant-expression}; neither is a structure
+or union that has a member whose type is not a \nonterm{constant-expression}.  Every other
+\Index{object type} is a \nonterm{constant-expression}. Objects with static storage duration shall
+be declared with a type that is a \nonterm{constant-expression}.
 \begin{rationale}
 Type declarations can declare identifiers with external linkage, whereas typedef declarations
@@ -3714,9 +3736,8 @@
 \end{rationale}
 
-An incomplete type\index{incomplete types} which is not a qualified version\index{qualified type} of
-a type is a value of type-class\index{type-class} \lstinline$dtype$. An object type\index{object
- types} which is not a qualified version of a type is a value of type-classes \lstinline$type$ and
-\lstinline$dtype$. A function type\index{function types} is a value of type-class
-\lstinline$ftype$.
+An \Index{incomplete type} which is not a qualified version\index{qualified type} of a type is a
+value of \Index{type-class} \lstinline$dtype$. An object type\index{object types} which is not a
+qualified version of a type is a value of type-classes \lstinline$type$ and \lstinline$dtype$. A
+\Index{function type} is a value of type-class \lstinline$ftype$.
 \begin{rationale}
 Syntactically, a type value is a \nonterm{type-name}, which is a declaration for an object which
@@ -3752,7 +3773,7 @@
 
 \begin{rationale}
-Since incomplete types\index{incomplete types} are not type values, they can not be used as the
-initializer in a type declaration, or as the type of a structure or union member. This prevents the
-declaration of types that contain each other.
+Since \Index{incomplete type}s are not type values, they can not be used as the initializer in a
+type declaration, or as the type of a structure or union member. This prevents the declaration of
+types that contain each other.
 \begin{lstlisting}
 type t1;
@@ -3900,6 +3921,6 @@
 A declaration\index{type declaration} of a type identifier \lstinline$T$ with type-class
 \lstinline$type$ implicitly declares a \define{default assignment} function
-\lstinline$T ?=?( T *, T )$\use{?=?}, with the same scope\index{scopes} and linkage\index{linkage} as
-the identifier \lstinline$T$.
+\lstinline$T ?=?( T *, T )$\use{?=?}, with the same \Index{scope} and \Index{linkage} as the
+identifier \lstinline$T$.
 \begin{rationale}
 Assignment is central to C's imperative programming style, and every existing C object type has
@@ -3912,11 +3933,11 @@
 \end{rationale}
 
-A definition\index{type definition} of a type identifier \lstinline$T$ with implementation
-type\index{implementation type} \lstinline$I$ and type-class \lstinline$type$ implicitly defines a
-default assignment function. A definition\index{type definition} of a type identifier \lstinline$T$
-with implementation type \lstinline$I$ and an assertion list implicitly defines \define{default
- functions} and \define{default objects} as declared by the assertion declarations. The default
-objects and functions have the same scope\index{scopes} and linkage\index{linkage} as the identifier
-\lstinline$T$. Their values are determined as follows:
+A definition\index{type definition} of a type identifier \lstinline$T$ with \Index{implementation
+type} \lstinline$I$ and type-class \lstinline$type$ implicitly defines a default assignment
+function. A definition\index{type definition} of a type identifier \lstinline$T$ with implementation
+type \lstinline$I$ and an assertion list implicitly defines \define{default function}s and
+\define{default object}s as declared by the assertion declarations. The default objects and
+functions have the same \Index{scope} and \Index{linkage} as the identifier \lstinline$T$. Their
+values are determined as follows:
 \begin{itemize}
 \item
@@ -4014,7 +4035,8 @@
 
 \section{Statements and blocks}
+
 Many statements contain expressions, which may have more than one interpretation. The following
-sections describe how the \CFA translator selects an interpretation. In all cases the result of
-the selection shall be a single unambiguous interpretation\index{interpretations}.
+sections describe how the \CFA translator selects an interpretation. In all cases the result of the
+selection shall be a single unambiguous \Index{interpretation}.
 
 
@@ -4032,7 +4054,6 @@
 \end{lstlisting}
 may have more than one interpretation, but it shall have only one interpretation with an integral
-type. An integer promotion\index{integer promotion} is performed on the expression if necessary.
-The constant expressions in \lstinline$case$ statements with the switch are converted to the
-promoted type.
+type. An \Index{integer promotion} is performed on the expression if necessary.  The constant
+expressions in \lstinline$case$ statements with the switch are converted to the promoted type.
 
 
@@ -4080,5 +4101,7 @@
 \appendix
 
+
 \chapter{Examples}
+
 
 \section{C types}
@@ -4183,8 +4206,8 @@
 \end{lstlisting}
 
-Specifications that define the dereference operator ( or subscript operator ) require two parameters,
-one for the pointer type and one for the pointed-at ( or element ) type. Different specifications are
-needed for each set of type qualifiers\index{type qualifiers}, because qualifiers are not included
-in types. The assertion ``\lstinline$|ptr_to( Safe_pointer, int )$'' should be read as
+Specifications that define the dereference operator ( or subscript operator ) require two
+parameters, one for the pointer type and one for the pointed-at ( or element ) type. Different
+specifications are needed for each set of \Index{type qualifier}s, because qualifiers are not
+included in types. The assertion ``\lstinline$|ptr_to( Safe_pointer, int )$'' should be read as
 ``\lstinline$Safe_pointer$ acts like a pointer to \lstinline$int$''.
 \begin{lstlisting}