RefMan, ch. 1 and 2: avoiding using the name "constant" when

"constructor" and "inductive" are meant also.

2 files changed, 8 insertions, 8 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 80e12898f..a2be25c3b 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1250,7 +1250,7 @@ possible, the correct argument will be automatically generated.
 
 \end{ErrMsgs}
 
-\subsection{Declaration of implicit arguments for a constant
+\subsection{Declaration of implicit arguments
 \comindex{Arguments}}
 \label{ImplicitArguments}
 
@@ -1263,7 +1263,7 @@ a priori and a posteriori.
 \subsubsection{Implicit Argument Binders}
 
 In the first setting, one wants to explicitly give the implicit
-arguments of a constant as part of its definition. To do this, one has
+arguments of a declared object as part of its definition. To do this, one has
 to surround the bindings of implicit arguments by curly braces:
 \begin{coq_eval}
 Reset Initial.
@@ -1300,7 +1300,7 @@ usual implicit arguments disambiguation syntax.
 
 \subsubsection{Declaring Implicit Arguments}
 
-To set implicit arguments for a constant a posteriori, one can use the
+To set implicit arguments a posteriori, one can use the
 command:
 \begin{quote}
 \tt Arguments {\qualid} \nelist{\possiblybracketedident}{}
@@ -1379,7 +1379,7 @@ Check (fun l => map length l = map (list nat) nat length l).
 \Rem To know which are the implicit arguments of an object, use the command
 {\tt Print Implicit} (see \ref{PrintImplicit}).
 
-\subsection{Automatic declaration of implicit arguments for a constant}
+\subsection{Automatic declaration of implicit arguments}
 
 {\Coq} can also automatically detect what are the implicit arguments
 of a defined object. The command is just
@@ -1582,7 +1582,7 @@ Implicit arguments names can be redefined using the following syntax:
 \end{quote}
 
 Without the {\tt rename} flag, {\tt Arguments} can be used to assert
-that a given constant has the expected number of arguments and that
+that a given object has the expected number of arguments and that
 these arguments are named as expected.
 
 \noindent {\bf Example (continued): }
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 9b527053c..e49c82d8f 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -971,7 +971,7 @@ are the names of its constructors and {\type$_1$}, {\ldots},
 {\type$_n$} their respective types. The types of the constructors have
 to satisfy a {\em positivity condition} (see Section~\ref{Positivity})
 for {\ident}.  This condition ensures the soundness of the inductive
-definition.  If this is the case, the constants {\ident},
+definition.  If this is the case, the names {\ident},
 {\ident$_1$}, {\ldots}, {\ident$_n$} are added to the environment with
 their respective types.  Accordingly to the universe where
 the inductive type lives ({\it e.g.} its type {\sort}), {\Coq} provides a
@@ -990,7 +990,7 @@ Inductive nat : Set :=
 \end{coq_example}
 
 The type {\tt nat} is defined as the least \verb:Set: containing {\tt
-  O} and closed by the {\tt S} constructor. The constants {\tt nat},
+  O} and closed by the {\tt S} constructor. The names {\tt nat},
 {\tt O} and {\tt S} are added to the environment.
 
 Now let us have a look at the elimination principles. They are three
@@ -1101,7 +1101,7 @@ Inductive list (A:Set) : Set :=
 \end{coq_example*}
 
 Note that in the type of {\tt nil} and {\tt cons}, we write {\tt
-  (list A)} and not just {\tt list}.\\ The constants {\tt nil} and
+  (list A)} and not just {\tt list}.\\ The constructors {\tt nil} and
 {\tt cons} will have respectively types:
 
 \begin{coq_example}