diff options
| author | ppedrot | 2012-02-01 16:50:57 +0000 |
|---|---|---|
| committer | ppedrot | 2012-02-01 16:50:57 +0000 |
| commit | 7d52b2b92177f45c23f820133f1a910d1c7a48f3 (patch) | |
| tree | 461d5be2ecdaae6f552e8d42212ffc7f62235622 | |
| parent | 3be4b91c09e6ec816aada997fc245484abfa1f05 (diff) | |
Corrected a careless cut-and-paste in Gallina description which dated back to 2003.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14963 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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}} |