<dt><tt>str1#str2</tt></dt>
<dd>"#" (paste) is a shorthand for !strconcat. It may concatenate
things that are not quoted strings, in which case an implicit
- !cast<string> is done on the operand of the paste.</dd>
+ !cast<string> is done on the operand of the paste.</dd>
<dt><tt>!cast<type>(a)</tt></dt>
<dd>A symbol of type <em>type</em> obtained by looking up the string 'a' in
the symbol table. If the type of 'a' does not match <em>type</em>, TableGen