Index: doc/refrat/refrat.tex
===================================================================
--- doc/refrat/refrat.tex	(revision 90c3b1c9b36943edd6040aac93c3da9265b218a4)
+++ doc/refrat/refrat.tex	(revision b63e3760197cb5f480cf1cdfd5886fdd0411d103)
@@ -62,4 +62,5 @@
 \renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}{-2.0ex \@plus -1ex \@minus -.2ex}{-1em}{\normalfont\normalsize\bfseries}}
 
+% index macros
 \newcommand{\italic}[1]{\emph{\hyperpage{#1}}}
 \newcommand{\definition}[1]{\textbf{\hyperpage{#1}}}
@@ -133,7 +134,7 @@
 % adjust listings macros
 \lstdefinelanguage{CFA}[ANSI]{C}%
-{morekeywords={asm,_Alignas,_Alignof,_At,_Atomic,_Bool,catch,catchResume,choose,_Complex,context,disable,dtype,enable,
-	fallthru,finally,forall,ftype,_Generic,_Imaginary,inline,lvalue,_Noreturn,restrict,_Static_assert,
-	_Thread_local,throw,throwResume,try,type,},
+{morekeywords={asm,_Alignas,_Alignof,_At,_Atomic,_Bool,catch,catchResume,choose,_Complex,trait,disable,dtype,enable,
+	fallthru,finally,forall,ftype,_Generic,_Imaginary,inline,lvalue,_Noreturn,otype,restrict,_Static_assert,
+	_Thread_local,throw,throwResume,try,},
 }%
 
@@ -280,5 +281,5 @@
 An instantiation of the generic type is written by specifying the type parameters in parentheses after the name of the generic type generator:
 \begin{lstlisting}
-forall( type T | sumable( T ) ) struct pair {
+forall( otype T | sumable( T ) ) struct pair {
 	T x;
 	T y;
@@ -292,5 +293,5 @@
 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:
 \begin{lstlisting}
-forall( type T ) void swap( pair(T) *p ) {
+forall( otype T ) void swap( pair(T) *p ) {
 	T z = p->x;
 	p->x = p->y;
@@ -302,11 +303,12 @@
 \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.
+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 {
+forall( otype T ) struct A;
+
+forall( otype T ) struct B {
 	A(T) *a;			// legal, but cannot instantiate B(T)
 };
@@ -314,5 +316,5 @@
 B(T) x;					// illegal, *x.a is of an incomplete generic type
  
-forall( type T ) struct A {
+forall( otype T ) struct A {
 	B( T ) *b;
 };
@@ -321,7 +323,7 @@
 
 // box.h:
-	forall( type T ) struct box;
-	forall( type T ) box( T ) *make_box( T );
-	forall( type T ) void use_box( box( T ) *b );
+	forall( otype T ) struct box;
+	forall( otype T ) box( T ) *make_box( T );
+	forall( otype T ) void use_box( box( T ) *b );
 	
 // main.c:
@@ -410,10 +412,9 @@
 
 \subsubsection{Specialization}
-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}.
+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.
+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 the bound assertion parameters replaced by their bound values.
@@ -422,11 +423,11 @@
 The type
 \begin{lstlisting}
-forall( type T, type U ) void (*)( T, U );
+forall( otype T, otype U ) void (*)( T, U );
 \end{lstlisting}
 can be specialized to (among other things)
 \begin{lstlisting}
-forall( type T ) void (*)( T, T );		// U bound to T
-forall( type T ) void (*)( T, real );	// U bound to real
-forall( type U ) void (*)( real, U );	// T bound to real
+forall( otype T ) void (*)( T, T );		// U bound to T
+forall( otype T ) void (*)( T, real );	// U bound to real
+forall( otype U ) void (*)( real, U );	// T bound to real
 void f( real, real );					// both bound to real 
 \end{lstlisting}
@@ -434,5 +435,5 @@
 The type
 \begin{lstlisting}
-forall( type T | T ?+?( T, T ) ) T (*)( T );
+forall( otype T | T ?+?( T, T ) ) T (*)( T );
 \end{lstlisting}
 can be specialized to (among other things)
@@ -494,6 +495,5 @@
 If \lstinline$int$ can represent all the values of \lstinline$unsigned short$, then the cost of an implicit conversion from \lstinline$unsigned short$ to \lstinline$unsigned$ is 2:
 \lstinline$unsigned short$ to \lstinline$int$ to \lstinline$unsigned$.
-Otherwise,
-\lstinline$unsigned short$ is converted directly to \lstinline$unsigned$, and the cost is 1.
+Otherwise, \lstinline$unsigned short$ is converted directly to \lstinline$unsigned$, and the cost is 1.
 
 \item
@@ -508,5 +508,5 @@
 	\rhs \lstinline$forall$
 	\rhs \lstinline$lvalue$
-	\rhs \lstinline$context$
+	\rhs \lstinline$trait$
 	\rhs \lstinline$dtype$
 	\rhs \lstinline$ftype$
@@ -539,6 +539,5 @@
 A \nonterm{constant-expression} that evaluates to 0 is effectively compatible with every pointer type.
 
-In C, the integer constants 0 and 1 suffice because the integer promotion rules can convert them to any arithmetic type, and the rules for pointer expressions treat constant expressions evaluating to
-0 as a special case.
+In C, the integer constants 0 and 1 suffice because the integer promotion rules can convert them to any arithmetic type, and the rules for pointer expressions treat constant expressions evaluating to 0 as a special case.
 However, user-defined arithmetic types often need the equivalent of a 1 or 0 for their functions or operators, polymorphic functions often need 0 and 1 constants of a type matching their polymorphic parameters, and user-defined pointer-like types may need a null value.
 Defining special constants for a user-defined type is more efficient than defining a conversion to the type from \lstinline$_Bool$.
@@ -836,20 +835,20 @@
 \predefined
 \begin{lstlisting}
-forall( type T ) lvalue T ?[?]( T *, ptrdiff_t );@\use{ptrdiff_t}@
-forall( type T ) lvalue _Atomic T ?[?]( _Atomic T *, ptrdiff_t );
-forall( type T ) lvalue const T ?[?]( const T *, ptrdiff_t );
-forall( type T ) lvalue restrict T ?[?]( restrict T *, ptrdiff_t );
-forall( type T ) lvalue volatile T ?[?]( volatile T *, ptrdiff_t );
-forall( type T ) lvalue _Atomic const T ?[?]( _Atomic const T *, ptrdiff_t );
-forall( type T ) lvalue _Atomic restrict T ?[?]( _Atomic restrict T *, ptrdiff_t );
-forall( type T ) lvalue _Atomic volatile T ?[?]( _Atomic volatile T *, ptrdiff_t );
-forall( type T ) lvalue const restrict T ?[?]( const restrict T *, ptrdiff_t );
-forall( type T ) lvalue const volatile T ?[?]( const volatile T *, ptrdiff_t );
-forall( type T ) lvalue restrict volatile T ?[?]( restrict volatile T *, ptrdiff_t );
-forall( type T ) lvalue _Atomic const restrict T ?[?]( _Atomic const restrict T *, ptrdiff_t );
-forall( type T ) lvalue _Atomic const volatile T ?[?]( _Atomic const volatile T *, ptrdiff_t );
-forall( type T ) lvalue _Atomic restrict volatile T ?[?]( _Atomic restrict volatile T *, ptrdiff_t );
-forall( type T ) lvalue const restrict volatile T ?[?]( const restrict volatile T *, ptrdiff_t );
-forall( type T ) lvalue _Atomic const restrict volatile T ?[?]( _Atomic const restrict volatile T *, ptrdiff_t );
+forall( otype T ) lvalue T ?[?]( T *, ptrdiff_t );@\use{ptrdiff_t}@
+forall( otype T ) lvalue _Atomic T ?[?]( _Atomic T *, ptrdiff_t );
+forall( otype T ) lvalue const T ?[?]( const T *, ptrdiff_t );
+forall( otype T ) lvalue restrict T ?[?]( restrict T *, ptrdiff_t );
+forall( otype T ) lvalue volatile T ?[?]( volatile T *, ptrdiff_t );
+forall( otype T ) lvalue _Atomic const T ?[?]( _Atomic const T *, ptrdiff_t );
+forall( otype T ) lvalue _Atomic restrict T ?[?]( _Atomic restrict T *, ptrdiff_t );
+forall( otype T ) lvalue _Atomic volatile T ?[?]( _Atomic volatile T *, ptrdiff_t );
+forall( otype T ) lvalue const restrict T ?[?]( const restrict T *, ptrdiff_t );
+forall( otype T ) lvalue const volatile T ?[?]( const volatile T *, ptrdiff_t );
+forall( otype T ) lvalue restrict volatile T ?[?]( restrict volatile T *, ptrdiff_t );
+forall( otype T ) lvalue _Atomic const restrict T ?[?]( _Atomic const restrict T *, ptrdiff_t );
+forall( otype T ) lvalue _Atomic const volatile T ?[?]( _Atomic const volatile T *, ptrdiff_t );
+forall( otype T ) lvalue _Atomic restrict volatile T ?[?]( _Atomic restrict volatile T *, ptrdiff_t );
+forall( otype T ) lvalue const restrict volatile T ?[?]( const restrict volatile T *, ptrdiff_t );
+forall( otype T ) lvalue _Atomic const restrict volatile T ?[?]( _Atomic const restrict volatile T *, ptrdiff_t );
 \end{lstlisting}
 \semantics
@@ -914,5 +913,5 @@
 \begin{rationale}
 One desirable property of a polymorphic programming language is \define{generalizability}: the ability to replace an abstraction with a more general but equivalent abstraction without requiring changes in any of the uses of the original\cite{Cormack90}.
-For instance, it should be possible to replace a function ``\lstinline$int f( int );$'' with ``\lstinline$forall( type T ) T f( T );$'' without affecting any calls of \lstinline$f$.
+For instance, it should be possible to replace a function ``\lstinline$int f( int );$'' with ``\lstinline$forall( otype T ) T f( T );$'' without affecting any calls of \lstinline$f$.
 
 \CFA\index{deficiencies!generalizability} does not fully possess this property, because
@@ -928,10 +927,10 @@
 f = g( d, f );		// (3) (unsafe conversion to float) 
 \end{lstlisting}
-If \lstinline$g$ was replaced by ``\lstinline$forall( type T ) T g( T, T );$'', the first and second calls would be unaffected, but the third would change: \lstinline$f$ would be converted to
+If \lstinline$g$ was replaced by ``\lstinline$forall( otype T ) T g( T, T );$'', the first and second calls would be unaffected, but the third would change: \lstinline$f$ would be converted to
 \lstinline$double$, and the result would be a \lstinline$double$.
 
 Another example is the function ``\lstinline$void h( int *);$''.
 This function can be passed a
-\lstinline$void *$ argument, but the generalization ``\lstinline$forall( type T ) void h( T *);$'' can not.
+\lstinline$void *$ argument, but the generalization ``\lstinline$forall( otype T ) void h( T *);$'' can not.
 In this case, \lstinline$void$ is not a valid value for \lstinline$T$ because it is not an object type.
 If unsafe conversions were allowed, \lstinline$T$ could be inferred to be \emph{any} object type, which is undesirable.
@@ -941,5 +940,5 @@
 A function called ``\lstinline$?()$'' might be part of a numerical differentiation package.
 \begin{lstlisting}
-extern type Derivative;
+extern otype Derivative;
 extern double ?()( Derivative, double );
 extern Derivative derivative_of( double (*f)( double ) );
@@ -962,5 +961,5 @@
 
 \begin{lstlisting}
-forall( type T ) T h( T );
+forall( otype T ) T h( T );
 double d = h( 1.5 );
 \end{lstlisting}
@@ -969,7 +968,7 @@
 
 \begin{lstlisting}
-forall( type T, type U ) void g( T, U );	// (4)
-forall( type T ) void g( T, T );			// (5)
-forall( type T ) void g( T, long );			// (6)
+forall( otype T, otype U ) void g( T, U );	// (4)
+forall( otype T ) void g( T, T );			// (5)
+forall( otype T ) void g( T, long );			// (6)
 void g( long, long );						// (7)
 double d;
@@ -991,11 +990,11 @@
 The fourth call has no interpretation for (5), because its arguments must have compatible type. (4) is chosen because it does not involve unsafe conversions.
 \begin{lstlisting}
-forall( type T ) T min( T, T );
+forall( otype T ) T min( T, T );
 double max( double, double );
-context min_max( T ) {@\impl{min_max}@
+trait min_max( T ) {@\impl{min_max}@
 	T min( T, T );
 	T max( T, T );
 }
-forall( type U | min_max( U ) ) void shuffle( U, U );
+forall( otype U | min_max( U ) ) void shuffle( U, U );
 shuffle( 9, 10 );
 \end{lstlisting}
@@ -1047,30 +1046,30 @@
 long double ?++( volatile long double * ), ?++( _Atomic volatile long double * );
 
-forall( type T ) T * ?++( T * restrict volatile * ), * ?++( T * _Atomic restrict volatile * );
-forall( type T ) _Atomic T * ?++( _Atomic T * restrict volatile * ), * ?++( _Atomic T * _Atomic restrict volatile * );
-forall( type T ) const T * ?++( const T * restrict volatile * ), * ?++( const T * _Atomic restrict volatile * );
-forall( type T ) volatile T * ?++( volatile T * restrict volatile * ), * ?++( volatile T * _Atomic restrict volatile * );
-forall( type T ) restrict T * ?++( restrict T * restrict volatile * ), * ?++( restrict T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const T * ?++( _Atomic const T * restrict volatile * ),
+forall( otype T ) T * ?++( T * restrict volatile * ), * ?++( T * _Atomic restrict volatile * );
+forall( otype T ) _Atomic T * ?++( _Atomic T * restrict volatile * ), * ?++( _Atomic T * _Atomic restrict volatile * );
+forall( otype T ) const T * ?++( const T * restrict volatile * ), * ?++( const T * _Atomic restrict volatile * );
+forall( otype T ) volatile T * ?++( volatile T * restrict volatile * ), * ?++( volatile T * _Atomic restrict volatile * );
+forall( otype T ) restrict T * ?++( restrict T * restrict volatile * ), * ?++( restrict T * _Atomic restrict volatile * );
+forall( otype T ) _Atomic const T * ?++( _Atomic const T * restrict volatile * ),
 	* ?++( _Atomic const T * _Atomic restrict volatile * );
-forall( type T ) _Atomic restrict T * ?++( _Atomic restrict T * restrict volatile * ),
+forall( otype T ) _Atomic restrict T * ?++( _Atomic restrict T * restrict volatile * ),
 	* ?++( _Atomic restrict T * _Atomic restrict volatile * );
-forall( type T ) _Atomic volatile T * ?++( _Atomic volatile T * restrict volatile * ),
+forall( otype T ) _Atomic volatile T * ?++( _Atomic volatile T * restrict volatile * ),
 	* ?++( _Atomic volatile T * _Atomic restrict volatile * );
-forall( type T ) const restrict T * ?++( const restrict T * restrict volatile * ),
+forall( otype T ) const restrict T * ?++( const restrict T * restrict volatile * ),
 	* ?++( const restrict T * _Atomic restrict volatile * );
-forall( type T ) const volatile T * ?++( const volatile T * restrict volatile * ),
+forall( otype T ) const volatile T * ?++( const volatile T * restrict volatile * ),
 	* ?++( const volatile T * _Atomic restrict volatile * );
-forall( type T ) restrict volatile T * ?++( restrict volatile T * restrict volatile * ),
+forall( otype T ) restrict volatile T * ?++( restrict volatile T * restrict volatile * ),
 	* ?++( restrict volatile T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const restrict T * ?++( _Atomic const restrict T * restrict volatile * ),
+forall( otype T ) _Atomic const restrict T * ?++( _Atomic const restrict T * restrict volatile * ),
 	* ?++( _Atomic const restrict T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const volatile T * ?++( _Atomic const volatile T * restrict volatile * ),
+forall( otype T ) _Atomic const volatile T * ?++( _Atomic const volatile T * restrict volatile * ),
 	* ?++( _Atomic const volatile T * _Atomic restrict volatile * );
-forall( type T ) _Atomic restrict volatile T * ?++( _Atomic restrict volatile T * restrict volatile * ),
+forall( otype T ) _Atomic restrict volatile T * ?++( _Atomic restrict volatile T * restrict volatile * ),
 	* ?++( _Atomic restrict volatile T * _Atomic restrict volatile * );
-forall( type T ) const restrict volatile T * ?++( const restrict volatile T * restrict volatile * ),
+forall( otype T ) const restrict volatile T * ?++( const restrict volatile T * restrict volatile * ),
 	* ?++( const restrict volatile T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const restrict volatile T * ?++( _Atomic const restrict volatile T * restrict volatile * ),
+forall( otype T ) _Atomic const restrict volatile T * ?++( _Atomic const restrict volatile T * restrict volatile * ),
 	* ?++( _Atomic const restrict volatile T * _Atomic restrict volatile * );
 
@@ -1091,30 +1090,30 @@
 long double ?--( volatile long double * ), ?--( _Atomic volatile long double * );
 
-forall( type T ) T * ?--( T * restrict volatile * ), * ?--( T * _Atomic restrict volatile * );
-forall( type T ) _Atomic T * ?--( _Atomic T * restrict volatile * ), * ?--( _Atomic T * _Atomic restrict volatile * );
-forall( type T ) const T * ?--( const T * restrict volatile * ), * ?--( const T * _Atomic restrict volatile * );
-forall( type T ) volatile T * ?--( volatile T * restrict volatile * ), * ?--( volatile T * _Atomic restrict volatile * );
-forall( type T ) restrict T * ?--( restrict T * restrict volatile * ), * ?--( restrict T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const T * ?--( _Atomic const T * restrict volatile * ),
+forall( otype T ) T * ?--( T * restrict volatile * ), * ?--( T * _Atomic restrict volatile * );
+forall( otype T ) _Atomic T * ?--( _Atomic T * restrict volatile * ), * ?--( _Atomic T * _Atomic restrict volatile * );
+forall( otype T ) const T * ?--( const T * restrict volatile * ), * ?--( const T * _Atomic restrict volatile * );
+forall( otype T ) volatile T * ?--( volatile T * restrict volatile * ), * ?--( volatile T * _Atomic restrict volatile * );
+forall( otype T ) restrict T * ?--( restrict T * restrict volatile * ), * ?--( restrict T * _Atomic restrict volatile * );
+forall( otype T ) _Atomic const T * ?--( _Atomic const T * restrict volatile * ),
 	* ?--( _Atomic const T * _Atomic restrict volatile * );
-forall( type T ) _Atomic restrict T * ?--( _Atomic restrict T * restrict volatile * ),
+forall( otype T ) _Atomic restrict T * ?--( _Atomic restrict T * restrict volatile * ),
 	* ?--( _Atomic restrict T * _Atomic restrict volatile * );
-forall( type T ) _Atomic volatile T * ?--( _Atomic volatile T * restrict volatile * ),
+forall( otype T ) _Atomic volatile T * ?--( _Atomic volatile T * restrict volatile * ),
 	* ?--( _Atomic volatile T * _Atomic restrict volatile * );
-forall( type T ) const restrict T * ?--( const restrict T * restrict volatile * ),
+forall( otype T ) const restrict T * ?--( const restrict T * restrict volatile * ),
 	* ?--( const restrict T * _Atomic restrict volatile * );
-forall( type T ) const volatile T * ?--( const volatile T * restrict volatile * ),
+forall( otype T ) const volatile T * ?--( const volatile T * restrict volatile * ),
 	* ?--( const volatile T * _Atomic restrict volatile * );
-forall( type T ) restrict volatile T * ?--( restrict volatile T * restrict volatile * ),
+forall( otype T ) restrict volatile T * ?--( restrict volatile T * restrict volatile * ),
 	* ?--( restrict volatile T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const restrict T * ?--( _Atomic const restrict T * restrict volatile * ),
+forall( otype T ) _Atomic const restrict T * ?--( _Atomic const restrict T * restrict volatile * ),
 	* ?--( _Atomic const restrict T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const volatile T * ?--( _Atomic const volatile T * restrict volatile * ),
+forall( otype T ) _Atomic const volatile T * ?--( _Atomic const volatile T * restrict volatile * ),
 	* ?--( _Atomic const volatile T * _Atomic restrict volatile * );
-forall( type T ) _Atomic restrict volatile T * ?--( _Atomic restrict volatile T * restrict volatile * ),
+forall( otype T ) _Atomic restrict volatile T * ?--( _Atomic restrict volatile T * restrict volatile * ),
 	* ?--( _Atomic restrict volatile T * _Atomic restrict volatile * );
-forall( type T ) const restrict volatile T * ?--( const restrict volatile T * restrict volatile * ),
+forall( otype T ) const restrict volatile T * ?--( const restrict volatile T * restrict volatile * ),
 	* ?--( const restrict volatile T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const restrict volatile T * ?--( _Atomic const restrict volatile T * restrict volatile * ),
+forall( otype T ) _Atomic const restrict volatile T * ?--( _Atomic const restrict volatile T * restrict volatile * ),
 	* ?--( _Atomic const restrict volatile T * _Atomic restrict volatile * );
 \end{lstlisting}
@@ -1195,5 +1194,5 @@
 The expression would be valid if \lstinline$?++$ were declared by
 \begin{lstlisting}
-forall( type T ) T * ?++( T * * );
+forall( otype T ) T * ?++( T * * );
 \end{lstlisting} with \lstinline$T$ inferred to be \lstinline$char$.
 
@@ -1203,5 +1202,5 @@
 Hence the actual predefined function is
 \begin{lstlisting}
-forall( type T ) T * ?++( T * restrict volatile * );
+forall( otype T ) T * ?++( T * restrict volatile * );
 \end{lstlisting} which also accepts a \lstinline$char * *$ argument, because of the safe conversions that add
 \lstinline$volatile$ and \lstinline$restrict$ qualifiers. (The parameter is not const-qualified, so constant pointers cannot be incremented.)
@@ -1217,5 +1216,5 @@
 \lstinline$char const volatile *$, so a new overloading is needed:
 \begin{lstlisting}
-forall( type T ) T const volatile * ?++( T const volatile *restrict volatile * );
+forall( otype T ) T const volatile * ?++( T const volatile *restrict volatile * );
 \end{lstlisting}
 One overloading is needed for each combination of qualifiers in the pointed-at type\index{deficiencies!pointers to qualified types}.
@@ -1225,5 +1224,5 @@
 The \lstinline$restrict$ qualifier is handled just like \lstinline$const$ and \lstinline$volatile$ in the previous case:
 \begin{lstlisting}
-forall( type T ) T restrict * ?++( T restrict *restrict volatile * );
+forall( otype T ) T restrict * ?++( T restrict *restrict volatile * );
 \end{lstlisting} with \lstinline$T$ inferred to be \lstinline$float *$.
 This looks odd, because {\c11} contains a constraint that requires restrict-qualified types to be pointer-to-object types, and \lstinline$T$ is not syntactically a pointer type. \CFA loosens the constraint.
@@ -1283,30 +1282,30 @@
 long double ++?( volatile long double * ), ++?( _Atomic volatile long double * );
 
-forall( type T ) T * ++?( T * restrict volatile * ), * ++?( T * _Atomic restrict volatile * );
-forall( type T ) _Atomic T * ++?( _Atomic T * restrict volatile * ), * ++?( _Atomic T * _Atomic restrict volatile * );
-forall( type T ) const T * ++?( const T * restrict volatile * ), * ++?( const T * _Atomic restrict volatile * );
-forall( type T ) volatile T * ++?( volatile T * restrict volatile * ), * ++?( volatile T * _Atomic restrict volatile * );
-forall( type T ) restrict T * ++?( restrict T * restrict volatile * ), * ++?( restrict T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const T * ++?( _Atomic const T * restrict volatile * ),
+forall( otype T ) T * ++?( T * restrict volatile * ), * ++?( T * _Atomic restrict volatile * );
+forall( otype T ) _Atomic T * ++?( _Atomic T * restrict volatile * ), * ++?( _Atomic T * _Atomic restrict volatile * );
+forall( otype T ) const T * ++?( const T * restrict volatile * ), * ++?( const T * _Atomic restrict volatile * );
+forall( otype T ) volatile T * ++?( volatile T * restrict volatile * ), * ++?( volatile T * _Atomic restrict volatile * );
+forall( otype T ) restrict T * ++?( restrict T * restrict volatile * ), * ++?( restrict T * _Atomic restrict volatile * );
+forall( otype T ) _Atomic const T * ++?( _Atomic const T * restrict volatile * ),
 	* ++?( _Atomic const T * _Atomic restrict volatile * );
-forall( type T ) _Atomic volatile T * ++?( _Atomic volatile T * restrict volatile * ),
+forall( otype T ) _Atomic volatile T * ++?( _Atomic volatile T * restrict volatile * ),
 	* ++?( _Atomic volatile T * _Atomic restrict volatile * );
-forall( type T ) _Atomic restrict T * ++?( _Atomic restrict T * restrict volatile * ),
+forall( otype T ) _Atomic restrict T * ++?( _Atomic restrict T * restrict volatile * ),
 	* ++?( _Atomic restrict T * _Atomic restrict volatile * );
-forall( type T ) const volatile T * ++?( const volatile T * restrict volatile * ),
+forall( otype T ) const volatile T * ++?( const volatile T * restrict volatile * ),
 	* ++?( const volatile T * _Atomic restrict volatile * );
-forall( type T ) const restrict T * ++?( const restrict T * restrict volatile * ),
+forall( otype T ) const restrict T * ++?( const restrict T * restrict volatile * ),
 	* ++?( const restrict T * _Atomic restrict volatile * );
-forall( type T ) restrict volatile T * ++?( restrict volatile T * restrict volatile * ),
+forall( otype T ) restrict volatile T * ++?( restrict volatile T * restrict volatile * ),
 	* ++?( restrict volatile T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const volatile T * ++?( _Atomic const volatile T * restrict volatile * ),
+forall( otype T ) _Atomic const volatile T * ++?( _Atomic const volatile T * restrict volatile * ),
 	* ++?( _Atomic const volatile T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const restrict T * ++?( _Atomic const restrict T * restrict volatile * ),
+forall( otype T ) _Atomic const restrict T * ++?( _Atomic const restrict T * restrict volatile * ),
 	* ++?( _Atomic const restrict T * _Atomic restrict volatile * );
-forall( type T ) _Atomic restrict volatile T * ++?( _Atomic restrict volatile T * restrict volatile * ),
+forall( otype T ) _Atomic restrict volatile T * ++?( _Atomic restrict volatile T * restrict volatile * ),
 	* ++?( _Atomic restrict volatile T * _Atomic restrict volatile * );
-forall( type T ) const restrict volatile T * ++?( const restrict volatile T * restrict volatile * ),
+forall( otype T ) const restrict volatile T * ++?( const restrict volatile T * restrict volatile * ),
 	* ++?( const restrict volatile T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const restrict volatile T * ++?( _Atomic const restrict volatile T * restrict volatile * ),
+forall( otype T ) _Atomic const restrict volatile T * ++?( _Atomic const restrict volatile T * restrict volatile * ),
 	* ++?( _Atomic const restrict volatile T * _Atomic restrict volatile * );
 
@@ -1327,30 +1326,30 @@
 long double --?( volatile long double * ), --?( _Atomic volatile long double * );
 
-forall( type T ) T * --?( T * restrict volatile * ), * --?( T * _Atomic restrict volatile * );
-forall( type T ) _Atomic T * --?( _Atomic T * restrict volatile * ), * --?( _Atomic T * _Atomic restrict volatile * );
-forall( type T ) const T * --?( const T * restrict volatile * ), * --?( const T * _Atomic restrict volatile * );
-forall( type T ) volatile T * --?( volatile T * restrict volatile * ), * --?( volatile T * _Atomic restrict volatile * );
-forall( type T ) restrict T * --?( restrict T * restrict volatile * ), * --?( restrict T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const T * --?( _Atomic const T * restrict volatile * ),
+forall( otype T ) T * --?( T * restrict volatile * ), * --?( T * _Atomic restrict volatile * );
+forall( otype T ) _Atomic T * --?( _Atomic T * restrict volatile * ), * --?( _Atomic T * _Atomic restrict volatile * );
+forall( otype T ) const T * --?( const T * restrict volatile * ), * --?( const T * _Atomic restrict volatile * );
+forall( otype T ) volatile T * --?( volatile T * restrict volatile * ), * --?( volatile T * _Atomic restrict volatile * );
+forall( otype T ) restrict T * --?( restrict T * restrict volatile * ), * --?( restrict T * _Atomic restrict volatile * );
+forall( otype T ) _Atomic const T * --?( _Atomic const T * restrict volatile * ),
 	* --?( _Atomic const T * _Atomic restrict volatile * );
-forall( type T ) _Atomic volatile T * --?( _Atomic volatile T * restrict volatile * ),
+forall( otype T ) _Atomic volatile T * --?( _Atomic volatile T * restrict volatile * ),
 	* --?( _Atomic volatile T * _Atomic restrict volatile * );
-forall( type T ) _Atomic restrict T * --?( _Atomic restrict T * restrict volatile * ),
+forall( otype T ) _Atomic restrict T * --?( _Atomic restrict T * restrict volatile * ),
 	* --?( _Atomic restrict T * _Atomic restrict volatile * );
-forall( type T ) const volatile T * --?( const volatile T * restrict volatile * ),
+forall( otype T ) const volatile T * --?( const volatile T * restrict volatile * ),
 	* --?( const volatile T * _Atomic restrict volatile * );
-forall( type T ) const restrict T * --?( const restrict T * restrict volatile * ),
+forall( otype T ) const restrict T * --?( const restrict T * restrict volatile * ),
 	* --?( const restrict T * _Atomic restrict volatile * );
-forall( type T ) restrict volatile T * --?( restrict volatile T * restrict volatile * ),
+forall( otype T ) restrict volatile T * --?( restrict volatile T * restrict volatile * ),
 	* --?( restrict volatile T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const volatile T * --?( _Atomic const volatile T * restrict volatile * ),
+forall( otype T ) _Atomic const volatile T * --?( _Atomic const volatile T * restrict volatile * ),
 	* --?( _Atomic const volatile T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const restrict T * --?( _Atomic const restrict T * restrict volatile * ),
+forall( otype T ) _Atomic const restrict T * --?( _Atomic const restrict T * restrict volatile * ),
 	* --?( _Atomic const restrict T * _Atomic restrict volatile * );
-forall( type T ) _Atomic restrict volatile T * --?( _Atomic restrict volatile T * restrict volatile * ),
+forall( otype T ) _Atomic restrict volatile T * --?( _Atomic restrict volatile T * restrict volatile * ),
 	* --?( _Atomic restrict volatile T * _Atomic restrict volatile * );
-forall( type T ) const restrict volatile T * --?( const restrict volatile T * restrict volatile * ),
+forall( otype T ) const restrict volatile T * --?( const restrict volatile T * restrict volatile * ),
 	* --?( const restrict volatile T * _Atomic restrict volatile * );
-forall( type T ) _Atomic const restrict volatile T * --?( _Atomic const restrict volatile T * restrict volatile * ),
+forall( otype T ) _Atomic const restrict volatile T * --?( _Atomic const restrict volatile T * restrict volatile * ),
 	* --?( _Atomic const restrict volatile T * _Atomic restrict volatile * );
 \end{lstlisting}
@@ -1380,20 +1379,20 @@
 \predefined
 \begin{lstlisting}
-forall( type T ) lvalue T *?( T * );
-forall( type T ) _Atomic lvalue T *?( _Atomic T * );
-forall( type T ) const lvalue T *?( const T * );
-forall( type T ) volatile lvalue T *?( volatile T * );
-forall( type T ) restrict lvalue T *?( restrict T * );
-forall( type T ) _Atomic const lvalue T *?( _Atomic const T * );
-forall( type T ) _Atomic volatile lvalue T *?( _Atomic volatile T * );
-forall( type T ) _Atomic restrict lvalue T *?( _Atomic restrict T * );
-forall( type T ) const volatile lvalue T *?( const volatile T * );
-forall( type T ) const restrict lvalue T *?( const restrict T * );
-forall( type T ) restrict volatile lvalue T *?( restrict volatile T * );
-forall( type T ) _Atomic const volatile lvalue T *?( _Atomic const volatile T * );
-forall( type T ) _Atomic const restrict lvalue T *?( _Atomic const restrict T * );
-forall( type T ) _Atomic restrict volatile lvalue T *?( _Atomic restrict volatile T * );
-forall( type T ) const restrict volatile lvalue T *?( const restrict volatile T * );
-forall( type T ) _Atomic const restrict volatile lvalue T *?( _Atomic const restrict volatile T * );
+forall( otype T ) lvalue T *?( T * );
+forall( otype T ) _Atomic lvalue T *?( _Atomic T * );
+forall( otype T ) const lvalue T *?( const T * );
+forall( otype T ) volatile lvalue T *?( volatile T * );
+forall( otype T ) restrict lvalue T *?( restrict T * );
+forall( otype T ) _Atomic const lvalue T *?( _Atomic const T * );
+forall( otype T ) _Atomic volatile lvalue T *?( _Atomic volatile T * );
+forall( otype T ) _Atomic restrict lvalue T *?( _Atomic restrict T * );
+forall( otype T ) const volatile lvalue T *?( const volatile T * );
+forall( otype T ) const restrict lvalue T *?( const restrict T * );
+forall( otype T ) restrict volatile lvalue T *?( restrict volatile T * );
+forall( otype T ) _Atomic const volatile lvalue T *?( _Atomic const volatile T * );
+forall( otype T ) _Atomic const restrict lvalue T *?( _Atomic const restrict T * );
+forall( otype T ) _Atomic restrict volatile lvalue T *?( _Atomic restrict volatile T * );
+forall( otype T ) const restrict volatile lvalue T *?( const restrict volatile T * );
+forall( otype T ) _Atomic const restrict volatile lvalue T *?( _Atomic const restrict volatile T * );
 forall( ftype FT ) FT *?( FT * );
 \end{lstlisting}
@@ -1510,7 +1509,7 @@
 \begin{rationale}
 \begin{lstlisting}
-type Pair = struct { int first, second; };
+otype Pair = struct { int first, second; };
 size_t p_size = sizeof(Pair);		// constant expression 
-extern type Rational;@\use{Rational}@
+extern otype Rational;@\use{Rational}@
 size_t c_size = sizeof(Rational);	// non-constant expression 
 forall(type T) T f(T p1, T p2) {
@@ -1636,5 +1635,5 @@
 Consider
 \begin{lstlisting}
-forall( type T | T ?*?( T, T ) ) T square( T );
+forall( otype T | T ?*?( T, T ) ) T square( T );
 short s;
 square( s );
@@ -1647,5 +1646,5 @@
 A more troubling example is
 \begin{lstlisting}
-forall( type T | ?*?( T, T ) ) T product( T[], int n );
+forall( otype T | ?*?( T, T ) ) T product( T[], int n );
 short sa[5];
 product( sa, 5);
@@ -1704,29 +1703,29 @@
 	?+?( _Complex long double, _Complex long double ), ?-?( _Complex long double, _Complex long double );
 
-forall( type T ) T * ?+?( T *, ptrdiff_t ), * ?+?( ptrdiff_t, T * ), * ?-?( T *, ptrdiff_t );
-forall( type T ) _Atomic T * ?+?( _Atomic T *, ptrdiff_t ), * ?+?( ptrdiff_t, _Atomic T * ),
+forall( otype T ) T * ?+?( T *, ptrdiff_t ), * ?+?( ptrdiff_t, T * ), * ?-?( T *, ptrdiff_t );
+forall( otype T ) _Atomic T * ?+?( _Atomic T *, ptrdiff_t ), * ?+?( ptrdiff_t, _Atomic T * ),
 	* ?-?( _Atomic T *, ptrdiff_t );
-forall( type T ) const T * ?+?( const T *, ptrdiff_t ), * ?+?( ptrdiff_t, const T * ),
+forall( otype T ) const T * ?+?( const T *, ptrdiff_t ), * ?+?( ptrdiff_t, const T * ),
 	* ?-?( const T *, ptrdiff_t );
-forall( type T ) restrict T * ?+?( restrict T *, ptrdiff_t ), * ?+?( ptrdiff_t, restrict T * ),
+forall( otype T ) restrict T * ?+?( restrict T *, ptrdiff_t ), * ?+?( ptrdiff_t, restrict T * ),
 	* ?-?( restrict T *, ptrdiff_t );
-forall( type T ) volatile T * ?+?( volatile T *, ptrdiff_t ), * ?+?( ptrdiff_t, volatile T * ),
+forall( otype T ) volatile T * ?+?( volatile T *, ptrdiff_t ), * ?+?( ptrdiff_t, volatile T * ),
 	* ?-?( volatile T *, ptrdiff_t );
-forall( type T ) _Atomic const T * ?+?( _Atomic const T *, ptrdiff_t ), * ?+?( ptrdiff_t, _Atomic const T * ),
+forall( otype T ) _Atomic const T * ?+?( _Atomic const T *, ptrdiff_t ), * ?+?( ptrdiff_t, _Atomic const T * ),
 	* ?-?( _Atomic const T *, ptrdiff_t );
-forall( type T ) _Atomic restrict T * ?+?( _Atomic restrict T *, ptrdiff_t ), * ?+?( ptrdiff_t, _Atomic restrict T * ),
+forall( otype T ) _Atomic restrict T * ?+?( _Atomic restrict T *, ptrdiff_t ), * ?+?( ptrdiff_t, _Atomic restrict T * ),
 	* ?-?( _Atomic restrict T *, ptrdiff_t );
-forall( type T ) _Atomic volatile T * ?+?( _Atomic volatile T *, ptrdiff_t ), * ?+?( ptrdiff_t, _Atomic volatile T * ),
+forall( otype T ) _Atomic volatile T * ?+?( _Atomic volatile T *, ptrdiff_t ), * ?+?( ptrdiff_t, _Atomic volatile T * ),
 	* ?-?( _Atomic volatile T *, ptrdiff_t );
-forall( type T ) const restrict T * ?+?( const restrict T *, ptrdiff_t ), * ?+?( ptrdiff_t, const restrict T * ),
+forall( otype T ) const restrict T * ?+?( const restrict T *, ptrdiff_t ), * ?+?( ptrdiff_t, const restrict T * ),
 	* ?-?( const restrict T *, ptrdiff_t );
-forall( type T ) const volatile T * ?+?( const volatile T *, ptrdiff_t ), * ?+?( ptrdiff_t, const volatile T * ),
+forall( otype T ) const volatile T * ?+?( const volatile T *, ptrdiff_t ), * ?+?( ptrdiff_t, const volatile T * ),
 	* ?-?( const volatile T *, ptrdiff_t );
-forall( type T ) restrict volatile T * ?+?( restrict volatile T *, ptrdiff_t ), * ?+?( ptrdiff_t, restrict volatile T * ),
+forall( otype T ) restrict volatile T * ?+?( restrict volatile T *, ptrdiff_t ), * ?+?( ptrdiff_t, restrict volatile T * ),
 	* ?-?( restrict volatile T *, ptrdiff_t );
-forall( type T ) _Atomic const restrict T * ?+?( _Atomic const restrict T *, ptrdiff_t ),
+forall( otype T ) _Atomic const restrict T * ?+?( _Atomic const restrict T *, ptrdiff_t ),
 	* ?+?( ptrdiff_t, _Atomic const restrict T * ),
 	* ?-?( _Atomic const restrict T *, ptrdiff_t );
-forall( type T ) ptrdiff_t
+forall( otype T ) ptrdiff_t
 	* ?-?( const restrict volatile T *, const restrict volatile T * ),
 	* ?-?( _Atomic const restrict volatile T *, _Atomic const restrict volatile T * );
@@ -2052,5 +2051,5 @@
 
 \begin{lstlisting}
-extern type Rational;@\use{Rational}@
+extern otype Rational;@\use{Rational}@
 extern const Rational 0;@\use{0}@
 extern int ?!=?( Rational, Rational );
@@ -2095,5 +2094,5 @@
 If the second and third operands both have interpretations with non-\lstinline$void$ types, the expression is treated as if it were the call ``\lstinline$cond((a)!=0, b, c)$'', with \lstinline$cond$ declared as
 \begin{lstlisting}
-forall( type T ) T cond( int, T, T );
+forall( otype T ) T cond( int, T, T );
 forall( dtype D ) void * cond( int, D *, void * ), * cond( int, void *, D * );
 forall( dtype D ) _atomic void * cond(
@@ -2455,80 +2454,80 @@
 \predefined
 \begin{lstlisting}
-forall( type T ) T
+forall( otype T ) T
 	* ?+=?( T * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T * restrict volatile *, ptrdiff_t ),
 	* ?+=?( T * _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T * _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T _Atomic
+forall( otype T ) T _Atomic
 	* ?+=?( T _Atomic * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic * restrict volatile *, ptrdiff_t ),
 	* ?+=?( T _Atomic * _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic * _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T const
+forall( otype T ) T const
 	* ?+=?( T const * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T const * restrict volatile *, ptrdiff_t ),
 	* ?+=?( T const * _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T const * _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T restrict
+forall( otype T ) T restrict
 	* ?+=?( T restrict * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T restrict * restrict volatile *, ptrdiff_t ),
 	* ?+=?( T restrict * _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T restrict * _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T volatile
+forall( otype T ) T volatile
 	* ?+=?( T volatile * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T volatile * restrict volatile *, ptrdiff_t ),
 	* ?+=?( T volatile * _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T volatile * _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T _Atomic const
+forall( otype T ) T _Atomic const
 	* ?+=?( T _Atomic const restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic const restrict volatile *, ptrdiff_t ),
 	* ?+=?( T _Atomic const _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic const _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T _Atomic restrict
+forall( otype T ) T _Atomic restrict
 	* ?+=?( T _Atomic restrict * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic restrict * restrict volatile *, ptrdiff_t ),
 	* ?+=?( T _Atomic restrict * _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic restrict * _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T _Atomic volatile
+forall( otype T ) T _Atomic volatile
 	* ?+=?( T _Atomic volatile * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic volatile * restrict volatile *, ptrdiff_t ),
 	* ?+=?( T _Atomic volatile * _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic volatile * _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T const restrict
+forall( otype T ) T const restrict
 	* ?+=?( T const restrict * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T const restrict * restrict volatile *, ptrdiff_t ),
 	* ?+=?( T const restrict * _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T const restrict * _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T const volatile
+forall( otype T ) T const volatile
 	* ?+=?( T const volatile * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T const volatile * restrict volatile *, ptrdiff_t ),
 	* ?+=?( T const volatile * _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T const volatile * _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T restrict volatile
+forall( otype T ) T restrict volatile
 	* ?+=?( T restrict volatile * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T restrict volatile * restrict volatile *, ptrdiff_t ),
 	* ?+=?( T restrict volatile * _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T restrict volatile * _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T _Atomic const restrict
+forall( otype T ) T _Atomic const restrict
 	* ?+=?( T _Atomic const restrict * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic const restrict * restrict volatile *, ptrdiff_t ),
 	* ?+=?( T _Atomic const restrict * _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic const restrict * _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T _Atomic const volatile
+forall( otype T ) T _Atomic const volatile
 	* ?+=?( T _Atomic const volatile * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic const volatile * restrict volatile *, ptrdiff_t ),
 	* ?+=?( T _Atomic const volatile * _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic const volatile * _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T _Atomic restrict volatile
+forall( otype T ) T _Atomic restrict volatile
 	* ?+=?( T _Atomic restrict volatile * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic restrict volatile * restrict volatile *, ptrdiff_t ),
 	* ?+=?( T _Atomic restrict volatile * _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic restrict volatile * _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T const restrict volatile
+forall( otype T ) T const restrict volatile
 	* ?+=?( T const restrict volatile * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T const restrict volatile * restrict volatile *, ptrdiff_t ),
 	* ?+=?( T const restrict volatile * _Atomic restrict volatile *, ptrdiff_t ),
 	* ?-=?( T const restrict volatile * _Atomic restrict volatile *, ptrdiff_t );
-forall( type T ) T _Atomic const restrict volatile
+forall( otype T ) T _Atomic const restrict volatile
 	* ?+=?( T _Atomic const restrict volatile * restrict volatile *, ptrdiff_t ),
 	* ?-=?( T _Atomic const restrict volatile * restrict volatile *, ptrdiff_t ),
@@ -2842,5 +2841,5 @@
 This sort of declaration is illegal because the scope of the type identifiers ends at the end of the declaration, but the scope of the structure tag does not.
 \begin{lstlisting}
-forall( type T ) struct Pair { T a, b;
+forall( otype T ) struct Pair { T a, b;
 } mkPair( T, T ); // illegal 
 \end{lstlisting}
@@ -2867,5 +2866,5 @@
 If this restriction were lifted, it would be possible to write
 \begin{lstlisting}
-forall( type T ) T * alloc( void );@\use{alloc}@ int *p = alloc();
+forall( otype T ) T * alloc( void );@\use{alloc}@ int *p = alloc();
 \end{lstlisting}
 Here \lstinline$alloc()$ would receive \lstinline$int$ as an inferred argument, and return an
@@ -2876,5 +2875,5 @@
 \lstinline$T$:
 \begin{lstlisting}
-forall( type T ) T * alloc( T initial_value );@\use{alloc}@
+forall( otype T ) T * alloc( T initial_value );@\use{alloc}@
 \end{lstlisting}
 \end{rationale}
@@ -2899,5 +2898,5 @@
 \begin{lstlisting}
 int fi( int );
-forall( type T ) T fT( T );
+forall( otype T ) T fT( T );
 \end{lstlisting}
 \lstinline$fi()$ takes an \lstinline$int$ and returns an \lstinline$int$. \lstinline$fT()$ takes a
@@ -2905,5 +2904,5 @@
 \begin{lstlisting}
 int (*pfi )( int ) = fi;
-forall( type T ) T (*pfT )( T ) = fT;
+forall( otype T ) T (*pfT )( T ) = fT;
 \end{lstlisting}
 \lstinline$pfi$ and \lstinline$pfT$ are pointers to functions. \lstinline$pfT$ is not polymorphic, but the function it points at is.
@@ -2912,5 +2911,5 @@
 	return pfi;
 }
-forall( type T ) T (*fvpfT( void ))( T ) {
+forall( otype T ) T (*fvpfT( void ))( T ) {
 	return pfT;
 }
@@ -2918,7 +2917,7 @@
 \lstinline$fvpfi()$ and \lstinline$fvpfT()$ are functions taking no arguments and returning pointers to functions. \lstinline$fvpfT()$ is monomorphic, but the function that its return value points at is polymorphic.
 \begin{lstlisting}
-forall( type T ) int ( *fTpfi( T ) )( int );
-forall( type T ) T ( *fTpfT( T ) )( T );
-forall( type T, type U ) U ( *fTpfU( T ) )( U );
+forall( otype T ) int ( *fTpfi( T ) )( int );
+forall( otype T ) T ( *fTpfT( T ) )( T );
+forall( otype T, otype U ) U ( *fTpfU( T ) )( U );
 \end{lstlisting}
 \lstinline$fTpfi()$ is a polymorphic function that returns a pointer to a monomorphic function taking an integer and returning an integer.
@@ -2930,6 +2929,6 @@
 \lstinline$char *$.
 \begin{lstlisting}
-forall( type T, type U, type V ) U * f( T *, U, V * const );
-forall( type U, type V, type W ) U * g( V *, U, W * const );
+forall( otype T, otype U, otype V ) U * f( T *, U, V * const );
+forall( otype U, otype V, otype W ) U * g( V *, U, W * const );
 \end{lstlisting}
 The functions \lstinline$f()$ and \lstinline$g()$ have compatible types.
@@ -2939,5 +2938,5 @@
 Replacing every \(f_i\) by \(g_i\) in \(f\) gives
 \begin{lstlisting}
-forall( type V, type U, type W ) U * f( V *, U, W * const );
+forall( otype V, otype U, otype W ) U * f( V *, U, W * const );
 \end{lstlisting} which has a return type and parameter list that is compatible with \(g\).
 \begin{rationale}
@@ -3127,13 +3126,13 @@
 \examples
 \begin{lstlisting}
-forall( type T | T ?*?( T, T ))@\use{?*?}@
+forall( otype T | T ?*?( T, T ))@\use{?*?}@
 T square( T val ) {@\impl{square}@
 	return val + val;
 }
-context summable( type T ) {@\impl{summable}@
+trait summable( otype T ) {@\impl{summable}@
 	T ?+=?( T *, T );@\use{?+=?}@
 	const T 0;@\use{0}@
 };
-context list_of( type List, type Element ) {@\impl{list_of}@
+trait list_of( otype List, otype Element ) {@\impl{list_of}@
 	Element car( List );
 	List cdr( List );
@@ -3142,5 +3141,5 @@
 	int is_nil( List );
 };
-context sum_list( type List, type Element | summable( Element ) | list_of( List, Element ) ) {};
+trait sum_list( otype List, otype Element | summable( Element ) | list_of( List, Element ) ) {};
 \end{lstlisting}
 \lstinline$sum_list$ contains seven declarations, which describe a list whose elements can be added up.
@@ -3204,13 +3203,13 @@
 Incomplete type declarations allow compact mutually-recursive types.
 \begin{lstlisting}
-type t1; // incomplete type declaration
-type t2 = struct { t1 * p; ... };
-type t1 = struct { t2 * p; ... };
+otype t1; // incomplete type declaration
+otype t2 = struct { t1 * p; ... };
+otype t1 = struct { t2 * p; ... };
 \end{lstlisting}
 Without them, mutual recursion could be handled by declaring mutually recursive structures, then initializing the types to those structures.
 \begin{lstlisting}
 struct s1;
-type t2 = struct s2 { struct s1 * p; ... };
-type t1 = struct s1 { struct s2 * p; ... };
+otype t2 = struct s2 { struct s1 * p; ... };
+otype t1 = struct s1 { struct s2 * p; ... };
 \end{lstlisting}
 This introduces extra names, and may force the programmer to cast between the types and their implementations.
@@ -3267,7 +3266,7 @@
 This prevents the declaration of types that contain each other.
 \begin{lstlisting}
-type t1;
-type t2 = t1; // illegal: incomplete type t1
-type t1 = t2;
+otype t1;
+otype t2 = t1; // illegal: incomplete type t1
+otype t1 = t2;
 \end{lstlisting}
 
@@ -3276,6 +3275,6 @@
  types}.
 \begin{lstlisting}
-extern type Huge; // extended-precision integer type
-type Rational = struct {
+extern otype Huge; // extended-precision integer type
+otype Rational = struct {
 	Huge numerator, denominator;	// illegal 
 };
@@ -3316,5 +3315,5 @@
 \begin{lstlisting}
 #include <stdlib.h>
-T * new( type T ) { return ( T * )malloc( sizeof( T) ); };
+T * new( otype T ) { return ( T * )malloc( sizeof( T) ); };
 @\ldots@ int * ip = new( int );
 \end{lstlisting}
@@ -3327,7 +3326,7 @@
 Since type declarations create new types, instances of types are always passed by value.
 \begin{lstlisting}
-type A1 = int[2];
+otype A1 = int[2];
 void f1( A1 a ) { a[0] = 0; };
-typedef int A2[2];
+otypedef int A2[2];
 void f2( A2 a ) { a[0] = 0; };
 A1 v1;
@@ -3346,5 +3345,5 @@
 That unit might contain the declarations
 \begin{lstlisting}
-type Complex = struct { float re, im; };@\impl{Complex}@
+otype Complex = struct { float re, im; };@\impl{Complex}@
 Complex cplx_i = { 0.0, 1.0 };@\impl{cplx_i}@
 float abs( Complex c ) {@\impl{abs( Complex )}@
@@ -3355,5 +3354,5 @@
 
 \begin{lstlisting}
-type Time_of_day = int;@\impl{Time_of_day}@ // seconds since midnight. 
+otype Time_of_day = int;@\impl{Time_of_day}@ // seconds since midnight. 
 Time_of_day ?+?( Time_of_day t1, int seconds ) {@\impl{?+?}@
 	return (( int)t1 + seconds ) % 86400;
@@ -3429,8 +3428,8 @@
 \examples
 \begin{lstlisting}
-context s( type T ) {
+trait s( otype T ) {
 	T a, b;
 } struct impl { int left, right; } a = { 0, 0 };
-type Pair | s( Pair ) = struct impl;
+otype Pair | s( Pair ) = struct impl;
 Pair b = { 1, 1 };
 \end{lstlisting}
@@ -3440,10 +3439,10 @@
 \lstinline$Pair b$ is compulsory because there is no \lstinline$struct impl b$ to construct a value from.
 \begin{lstlisting}
-context ss( type T ) {
+trait ss( otype T ) {
 	T clone( T );
 	void munge( T * );
 }
-type Whatsit | ss( Whatsit );@\use{Whatsit}@
-type Doodad | ss( Doodad ) = struct doodad {@\use{Doodad}@
+otype Whatsit | ss( Whatsit );@\use{Whatsit}@
+otype Doodad | ss( Doodad ) = struct doodad {@\use{Doodad}@
 	Whatsit; // anonymous member 
 	int extra;
@@ -3466,5 +3465,5 @@
 Default functions and objects are subject to the normal scope rules.
 \begin{lstlisting}
-type T = @\ldots@;
+otype T = @\ldots@;
 T a_T = @\ldots@;		// Default assignment used. 
 T ?=?( T *, T );
@@ -3735,5 +3734,5 @@
 The assertion ``\lstinline$scalar( Complex )$'' should be read as ``type \lstinline$Complex$ is scalar''.
 \begin{lstlisting}
-context scalar( type T ) {@\impl{scalar}@
+trait scalar( otype T ) {@\impl{scalar}@
 	int !?( T );
 	int ?<?( T, T ), ?<=?( T, T ), ?==?( T, T ), ?>=?( T, T ), ?>?( T, T ), ?!=?( T, T );
@@ -3745,5 +3744,5 @@
 This is equivalent to inheritance of specifications.
 \begin{lstlisting}
-context arithmetic( type T | scalar( T ) ) {@\impl{arithmetic}@@\use{scalar}@
+trait arithmetic( otype T | scalar( T ) ) {@\impl{arithmetic}@@\use{scalar}@
 	T +?( T ), -?( T );
 	T ?*?( T, T ), ?/?( T, T ), ?+?( T, T ), ?-?( T, T );
@@ -3754,5 +3753,5 @@
 \define{integral types}.
 \begin{lstlisting}
-context integral( type T | arithmetic( T ) ) {@\impl{integral}@@\use{arithmetic}@
+trait integral( otype T | arithmetic( T ) ) {@\impl{integral}@@\use{arithmetic}@
 	T ~?( T );
 	T ?&?( T, T ), ?|?( T, T ), ?^?( T, T );
@@ -3768,5 +3767,5 @@
 The only operation that can be applied to all modifiable lvalues is simple assignment.
 \begin{lstlisting}
-context m_lvalue( type T ) {@\impl{m_lvalue}@
+trait m_lvalue( otype T ) {@\impl{m_lvalue}@
 	T ?=?( T *, T );
 };
@@ -3778,5 +3777,5 @@
 Scalars can also be incremented and decremented.
 \begin{lstlisting}
-context m_l_scalar( type T | scalar( T ) | m_lvalue( T ) ) {@\impl{m_l_scalar}@
+trait m_l_scalar( otype T | scalar( T ) | m_lvalue( T ) ) {@\impl{m_l_scalar}@
 	T ?++( T * ), ?--( T * );@\use{scalar}@@\use{m_lvalue}@
 	T ++?( T * ), --?( T * );
@@ -3787,9 +3786,9 @@
 Note that this results in the ``inheritance'' of \lstinline$scalar$ along both paths.
 \begin{lstlisting}
-context m_l_arithmetic( type T | m_l_scalar( T ) | arithmetic( T ) ) {@\impl{m_l_arithmetic}@
+trait m_l_arithmetic( otype T | m_l_scalar( T ) | arithmetic( T ) ) {@\impl{m_l_arithmetic}@
 	T ?/=?( T *, T ), ?*=?( T *, T );@\use{m_l_scalar}@@\use{arithmetic}@
 	T ?+=?( T *, T ), ?-=?( T *, T );
 };
-context m_l_integral( type T | m_l_arithmetic( T ) | integral( T ) ) {@\impl{m_l_integral}@
+trait m_l_integral( otype T | m_l_arithmetic( T ) | integral( T ) ) {@\impl{m_l_integral}@
 	T ?&=?( T *, T ), ?|=?( T *, T ), ?^=?( T *, T );@\use{m_l_arithmetic}@
 	T ?%=?( T *, T ), ?<<=?( T *, T ), ?>>=?( T *, T );@\use{integral}@
@@ -3811,9 +3810,9 @@
 \lstinline$arithmetic$, so these operators cannot be consolidated in \lstinline$scalar$.
 \begin{lstlisting}
-context pointer( type P | scalar( P ) ) {@\impl{pointer}@@\use{scalar}@
+trait pointer( type P | scalar( P ) ) {@\impl{pointer}@@\use{scalar}@
 	P ?+?( P, long int ), ?+?( long int, P ), ?-?( P, long int );
 	ptrdiff_t ?-?( P, P );
 };
-context m_l_pointer( type P | pointer( P ) | m_l_scalar( P ) ) {@\impl{m_l_pointer}@
+trait m_l_pointer( type P | pointer( P ) | m_l_scalar( P ) ) {@\impl{m_l_pointer}@
 	P ?+=?( P *, long int ), ?-=?( P *, long int );
 	P ?=?( P *, void * );
@@ -3827,17 +3826,17 @@
 ``\lstinline$Safe_pointer$ acts like a pointer to \lstinline$int$''.
 \begin{lstlisting}
-context ptr_to( type P | pointer( P ), type T ) {@\impl{ptr_to}@@\use{pointer}@
+trait ptr_to( type P | pointer( P ), otype T ) {@\impl{ptr_to}@@\use{pointer}@
 	lvalue T *?( P );
 	lvalue T ?[?]( P, long int );
 };
-context ptr_to_const( type P | pointer( P ), type T ) {@\impl{ptr_to_const}@
+trait ptr_to_const( type P | pointer( P ), otype T ) {@\impl{ptr_to_const}@
 	const lvalue T *?( P );
 	const lvalue T ?[?]( P, long int );@\use{pointer}@
 };
-context ptr_to_volatile( type P | pointer( P ), type T ) }@\impl{ptr_to_volatile}@
+trait ptr_to_volatile( type P | pointer( P ), otype T ) }@\impl{ptr_to_volatile}@
 	volatile lvalue T *?( P );
 	volatile lvalue T ?[?]( P, long int );@\use{pointer}@
 };
-context ptr_to_const_volatile( type P | pointer( P ), type T ) }@\impl{ptr_to_const_volatile}@
+trait ptr_to_const_volatile( type P | pointer( P ), otype T ) }@\impl{ptr_to_const_volatile}@
 	const volatile lvalue T *?( P );@\use{pointer}@
 	const volatile lvalue T ?[?]( P, long int );
@@ -3849,17 +3848,17 @@
 ``\lstinline$ptr_to$'' specifications.
 \begin{lstlisting}
-context m_l_ptr_to( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to}@ type T | ptr_to( P, T )@\use{ptr_to}@ {
+trait m_l_ptr_to( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to}@ otype T | ptr_to( P, T )@\use{ptr_to}@ {
 	P ?=?( P *, T * );
 	T * ?=?( T **, P );
 };
-context m_l_ptr_to_const( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to_const}@ type T | ptr_to_const( P, T )@\use{ptr_to_const}@) {
+trait m_l_ptr_to_const( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to_const}@ otype T | ptr_to_const( P, T )@\use{ptr_to_const}@) {
 	P ?=?( P *, const T * );
 	const T * ?=?( const T **, P );
 };
-context m_l_ptr_to_volatile( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to_volatile}@ type T | ptr_to_volatile( P, T )) {@\use{ptr_to_volatile}@
+trait m_l_ptr_to_volatile( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to_volatile}@ otype T | ptr_to_volatile( P, T )) {@\use{ptr_to_volatile}@
 	P ?=?( P *, volatile T * );
 	volatile T * ?=?( volatile T **, P );
 };
-context m_l_ptr_to_const_volatile( type P | ptr_to_const_volatile( P ),@\use{ptr_to_const_volatile}@@\impl{m_l_ptr_to_const_volatile}@
+trait m_l_ptr_to_const_volatile( type P | ptr_to_const_volatile( P ),@\use{ptr_to_const_volatile}@@\impl{m_l_ptr_to_const_volatile}@
 		type T | m_l_ptr_to_volatile( P, T ) | m_l_ptr_to_const( P )) {@\use{m_l_ptr_to_const}@@\use{m_l_ptr_to_volatile}@
 	P ?=?( P *, const volatile T * );
@@ -3871,5 +3870,5 @@
 An alternative specification can make use of the fact that qualification of the pointed-at type is part of a pointer type to capture that regularity.
 \begin{lstlisting}
-context m_l_ptr_like( type MyP | m_l_pointer( MyP ),@\use{m_l_pointer}@@\impl{m_l_ptr_like}@ type CP | m_l_pointer( CP ) ) {
+trait m_l_ptr_like( type MyP | m_l_pointer( MyP ),@\use{m_l_pointer}@@\impl{m_l_ptr_like}@ type CP | m_l_pointer( CP ) ) {
 	MyP ?=?( MyP *, CP );
 	CP ?=?( CP *, MyP );
@@ -3904,13 +3903,13 @@
 C and \CFA have an extra, non-obvious comparison operator: ``\lstinline$!$'', logical negation, returns 1 if its operand compares equal to 0, and 0 otherwise.
 \begin{lstlisting}
-context comparable( type T ) {
+trait comparable( otype T ) {
 	const T 0;
 	int compare( T, T );
 }
-forall( type T | comparable( T ) ) int ?<?( T l, T r ) {
+forall( otype T | comparable( T ) ) int ?<?( T l, T r ) {
 	return compare( l, r ) < 0;
 }
 // ... similarly for <=, ==, >=, >, and !=. 
-forall( type T | comparable( T ) ) int !?( T operand ) {
+forall( otype T | comparable( T ) ) int !?( T operand ) {
 	return !compare( operand, 0 );
 }
@@ -3924,25 +3923,25 @@
 Similarly, a complete integral type would provide integral operations based on integral assignment operations.
 \begin{lstlisting}
-context arith_base( type T ) {
+trait arith_base( otype T ) {
 	const T 1;
 	T ?+=?( T *, T ), ?-=?( T *, T ), ?*=?( T *, T ), ?/=?( T *, T );
 }
-forall( type T | arith_base( T ) ) T ?+?( T l, T r ) {
+forall( otype T | arith_base( T ) ) T ?+?( T l, T r ) {
 	return l += r;
 }
-forall( type T | arith_base( T ) ) T ?++( T * operand ) {
+forall( otype T | arith_base( T ) ) T ?++( T * operand ) {
 	T temporary = *operand;
 	*operand += 1;
 	return temporary;
 }
-forall( type T | arith_base( T ) ) T ++?( T * operand ) {
+forall( otype T | arith_base( T ) ) T ++?( T * operand ) {
 	return *operand += 1;
 }
 // ... similarly for -, --, *, and /. 
-context int_base( type T ) {
+trait int_base( otype T ) {
 	T ?&=?( T *, T ), ?|=?( T *, T ), ?^=?( T *, T );
 	T ?%=?( T *, T ), ?<<=?( T *, T ), ?>>=?( T *, T );
 }
-forall( type T | int_base( T ) ) T ?&?( T l, T r ) {
+forall( otype T | int_base( T ) ) T ?&?( T l, T r ) {
 	return l &= r;
 }