From 319b3657123b5d5b7336409fa4e17da8b19bca28 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 21 Oct 2011 08:36:10 -0400 Subject: Note a parsing restriction in the manual --- doc/manual.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/manual.tex b/doc/manual.tex index 872dca93..71df6ccc 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -426,7 +426,7 @@ $$\begin{array}{rrcll} &&& M.x & \textrm{projection from a module} \\ \end{array}$$ -We include both abstraction and application for kind polymorphism, but applications are only inferred internally; they may not be written explicitly in source programs. +We include both abstraction and application for kind polymorphism, but applications are only inferred internally; they may not be written explicitly in source programs. Also, in the ``known-length type-level record'' form, in $c_1 = c_2$ terms, the parser currently only allows $c_1$ to be of the forms $X$ (as a shorthand for $\#X$) or $x$, or a natural number to stand for the corresponding field name (e.g., for tuples). Modules of the module system are described by \emph{signatures}. $$\begin{array}{rrcll} -- cgit v1.2.3