aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-04-06 18:42:54 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-04-06 18:42:54 +0000
commite29a6555392664b5723da7bcfe5b5a8f04eb4b6b (patch)
treec09b3e0fe8e668e773279417c6f5da733efb4387
parentfc8e7fbc85ac147d7d07735e6a9790c013f9c97a (diff)
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8541 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--doc/RefMan-gal.tex1
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index a73f4f18a..543b3fb82 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -381,7 +381,6 @@ subclass of the syntactic class {\term}.
\index{specif@{\specif}}
\item {\Type} is the type of {\Set} and {\Prop}
\end{itemize}
-More on sorts can be found in section~\ref{Sorts}.
\noindent More on sorts can be found in section \ref{Sorts}.
\subsection{Binders