Index: doc/refrat/refrat.tex
===================================================================
--- doc/refrat/refrat.tex	(revision 01414f159c56144d8a47ad9672b644219e73c998)
+++ doc/refrat/refrat.tex	(revision 41b3ddd04624d97d5e1685d41a9a93eb856d9e64)
@@ -10,4 +10,5 @@
 \usepackage{varioref}
 \usepackage{listings}
+\usepackage{comment}
 \usepackage{latexsym}					% \Box
 \usepackage{mathptmx}					% better math font with "times"
@@ -112,5 +113,5 @@
 
 \lstdefinelanguage{CFA}[ANSI]{C}%
-  {morekeywords={asm,_Atomic,catch,catchResume,choose,_Complex,context,disable,dtype,enable,
+  {morekeywords={asm,_At,_Atomic,catch,catchResume,choose,_Complex,context,disable,dtype,enable,
 	fallthru,finally,forall,ftype,_Imaginary,lvalue,restrict,throw,throwResume,try,type,},
 }
@@ -184,12 +185,19 @@
 
 % No ``Scope'' or ``Normative references'' chapters yet.
+
+
 \setcounter{chapter}{2}
 \chapter{Terms, definitions, and symbols}
+
 Terms from the {\c11} standard used in this document have the same meaning as in the {\c11}
 standard.
 
 % No ``Conformance'' or ``Environment'' chapters yet.
+
+
 \setcounter{chapter}{5}
 \chapter{Language}
+
+
 \section{Notation}
 The syntax notation used in this document is the same as is used in the {\c11} standard, with one
@@ -235,4 +243,78 @@
 \end{rationale}
 
+
+\setcounter{subsection}{8}
+\subsection{Generic Types}
+
+
+\subsubsection{Semantics}
+
+CFA provides a capability for generic types; using this capability a single "generic type generator"
+can be written that can represent multiple concrete type instantiations by substitution of the "type
+parameters" of the generic type for concrete types. Syntactically a generic type generator is
+represented by putting a forall specifier on a struct or union declaration, as defined in section
+6.7.2.5. An instantiation of the generic type is written by specifying the type parameters in
+parentheses after the name of the generic type generator, as in the following example:
+\begin{lstlisting}
+forall( type T ) struct pair {
+	T x;
+	T y;
+};
+
+pair( int ) p = { 3, 14 };
+\end{lstlisting}
+
+The type parameters in an instantiation of a generic type must satisfy any constraints in the forall
+specifier on the type generator declaration. The instantiation then has the semantics that would
+result if the type parameters were substituted into the type generator declaration by macro
+substitution.
+
+Polymorphic functions may have generic types as parameters, and those generic types may use type
+parameters of the polymorphic function as type parameters of the generic type, as in the following
+example:
+\begin{lstlisting}
+forall( type T ) void swap( pair(T) *p ) {
+	T z = p->x;
+	p->x = p->y;
+	p->y = z;
+}
+\end{lstlisting}
+
+
+\subsubsection{Constraints}
+
+To avoid unduly constraining implementors, the generic type generator definition must be visible at
+any point where it is instantiated.  Forward declarations of generic type generators are not
+forbidden, but the definition must be visible to instantiate the generic type.  Equivalently,
+instantiations of generic types are not allowed to be incomplete types.
+
+\examples
+\begin{lstlisting}
+forall( type T ) struct A;
+
+forall( type T ) struct B {
+	A(T) *a;  // legal, but cannot instantiate B(T)
+};
+
+B(T) x; // illegal, *x.a is of an incomplete generic type
+
+forall( type T ) struct A {
+	B( T ) *b;
+};
+
+B( T ) y; // legal, *x.a is now of a complete generic type
+
+
+// box.h:
+	forall( type T ) struct box;
+	forall( type T ) box( T ) *make_box( T );
+	forall( type T ) void use_box( box( T ) *b );
+	
+// main.c:
+	box( int ) *b = make_box( 42 ); // illegal, def'n of box not visible
+	use_box( b ); // illegal
+\end{lstlisting}
+
+
 \section{Conversions}
 \CFA defines situations where values of one type are automatically converted to another type.
@@ -242,8 +324,9 @@
 
 \subsection{Arithmetic operands}
-\setcounter{subsubsection}{7}
-
-
+
+
+\setcounter{subsubsection}{8}
 \subsubsection{Safe arithmetic conversions}
+
 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
@@ -302,7 +385,7 @@
 
 \subsection{Other operands}
+
+
 \setcounter{subsubsection}{3}
-
-
 \subsubsection{Anonymous structures and unions}
 \label{anon-conv}
@@ -3319,5 +3402,6 @@
 
 \setcounter{subsubsection}{4}
-\subsubsection{Forall specifiers}\label{forall}
+\subsubsection{Forall specifiers}
+\label{forall}
 
 \begin{syntax}
@@ -3326,4 +3410,5 @@
 \end{syntax}
 
+\begin{comment}
 \constraints
 If the \nonterm{declaration-specifiers} of a declaration that contains a \nonterm{forall-specifier}
@@ -3339,4 +3424,5 @@
 members' type be?
 \end{rationale}
+\end{comment}
 
 \semantics
@@ -3344,6 +3430,6 @@
 identifiers, function and object identifiers with \Index{no linkage}.
 
-If, in the declaration ``\lstinline$T D1$'', \lstinline$T$ contains \nonterm{forall-specifier}s and
-\lstinline$D1$ has the form
+If, in the declaration ``\lstinline$T D$'', \lstinline$T$ contains \nonterm{forall-specifier}s and
+\lstinline$D$ has the form
 \begin{lstlisting}
 D( @\normalsize\nonterm{parameter-type-list}@ )
@@ -3356,4 +3442,6 @@
 assertions that use an inferred parameter of a function declarator are \Index{assertion parameter}s
 of that function declarator.
+
+\begin{comment}
 \begin{rationale}
 Since every inferred parameter is used by some parameter, inference can be understood as a single
@@ -3376,4 +3464,5 @@
 \end{lstlisting}
 \end{rationale}
+\end{comment}
 
 If a function declarator is part of a function definition, its inferred parameters and assertion