RefMan, ch. 4: Removing confusing paragraph "Constants": in it,

constants are yet given another definition; the reference to other
presentation is more confusing than helpful to me.

1 files changed, 27 insertions, 25 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index ca3a6135d8..3b8a8fee11 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -148,31 +148,33 @@ constraints must remain acyclic.  Typing expressions that violate the
 acyclicity of the graph of constraints results in a \errindex{Universe
 inconsistency} error (see also Section~\ref{PrintingUniverses}).
 
-\subsection{Constants}
-
-Constants refers to
-objects in the global environment. These constants may denote previously
-defined objects, but also objects related to inductive definitions
-(either the type itself or one of its constructors or destructors).
-
-\medskip\noindent {\bf Remark. } In other presentations of \CIC, 
-the inductive objects are not seen as
-external declarations but as first-class terms. Usually the
-definitions are also completely ignored.  This is a nice theoretical
-point of view but not so practical. An inductive definition is
-specified by a possibly huge set of declarations, clearly we want to
-share this specification among the various inductive objects and not
-to duplicate it. So the specification should exist somewhere and the
-various objects should refer to it.  We choose one more level of
-indirection where the objects are just represented as constants and
-the environment gives the information on the kind of object the
-constant refers to.
-
-\medskip
-Our inductive objects will be manipulated as constants declared in the
-environment. This roughly corresponds to the way they are actually
-implemented in the \Coq\ system. It is simple to map this presentation
-in a theory where inductive objects are represented by terms.
+%% HH: This looks to me more like source of confusion than helpful
+
+%% \subsection{Constants}
+
+%% Constants refers to
+%% objects in the global environment. These constants may denote previously
+%% defined objects, but also objects related to inductive definitions
+%% (either the type itself or one of its constructors or destructors).
+
+%% \medskip\noindent {\bf Remark. } In other presentations of \CIC, 
+%% the inductive objects are not seen as
+%% external declarations but as first-class terms. Usually the
+%% definitions are also completely ignored.  This is a nice theoretical
+%% point of view but not so practical. An inductive definition is
+%% specified by a possibly huge set of declarations, clearly we want to
+%% share this specification among the various inductive objects and not
+%% to duplicate it. So the specification should exist somewhere and the
+%% various objects should refer to it.  We choose one more level of
+%% indirection where the objects are just represented as constants and
+%% the environment gives the information on the kind of object the
+%% constant refers to.
+
+%% \medskip
+%% Our inductive objects will be manipulated as constants declared in the
+%% environment. This roughly corresponds to the way they are actually
+%% implemented in the \Coq\ system. It is simple to map this presentation
+%% in a theory where inductive objects are represented by terms.
 
 \subsection{Terms}