diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 204fa90d90..6fe9c08d35 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -396,13 +396,6 @@ subclass of the syntactic class {\term}. \end{itemize} \noindent More on sorts can be found in Section~\ref{Sorts}. -\bigskip - -{\Coq} terms are typed. {\Coq} types are recognized by the same -syntactic class as {\term}. We denote by {\type} the semantic subclass -of types inside the syntactic class {\term}. -\index{type@{\type}} - \subsection{Binders \label{Binders} \index{binders}} |