From 7d52b2b92177f45c23f820133f1a910d1c7a48f3 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 1 Feb 2012 16:50:57 +0000
Subject: 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
---
 doc/refman/RefMan-gal.tex | 7 -------
 1 file changed, 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}}
-- 
cgit v1.2.3