Uniformisation in the documentation: remove the use of 'coinductive' in

favour of 'co-inductive'.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15162 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 16 insertions, 16 deletions

diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index 276a9e3a8..56b989b2e 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -14,7 +14,7 @@ This section describes the full form of pattern-matching in {\Coq} terms.
 match} is presented in Figures~\ref{term-syntax}
 and~\ref{term-syntax-aux}.  Identifiers in patterns are either
 constructor names or variables. Any identifier that is not the
-constructor of an inductive or coinductive type is considered to be a
+constructor of an inductive or co-inductive type is considered to be a
 variable. A variable name cannot occur more than once in a given
 pattern. It is recommended to start variable names by a lowercase
 letter.
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 9660a04bd..901969703 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -41,7 +41,7 @@ The beginner can skip them.
 The reader seeking a background on the Calculus of Inductive
 Constructions may read several papers. Giménez and Castéran~\cite{GimCas05} 
 provide
-an introduction to inductive and coinductive definitions in Coq. In
+an introduction to inductive and co-inductive definitions in Coq. In
 their book~\cite{CoqArt}, Bertot and Castéran give a precise
 description of the \CIC{} based on numerous practical examples.
 Barras~\cite{Bar99}, Werner~\cite{Wer94} and
@@ -1650,12 +1650,12 @@ Abort.
 The principles of mutual induction can be automatically generated 
 using the {\tt Scheme} command described in Section~\ref{Scheme}.
 
-\section{Coinductive types}
-The implementation contains also coinductive definitions, which are
+\section{Co-inductive types}
+The implementation contains also co-inductive definitions, which are
 types inhabited by infinite objects. 
-More information on coinductive definitions can be found
+More information on co-inductive definitions can be found
 in~\cite{Gimenez95b,Gim98,GimCas05}.
-%They are described in Chapter~\ref{Coinductives}.
+%They are described in Chapter~\ref{Co-inductives}.
 
 \section[\iCIC : the Calculus of Inductive Construction with
   impredicative \Set]{\iCIC : the Calculus of Inductive Construction with
diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex
index 619a8ee10..e609fce82 100644
--- a/doc/refman/RefMan-coi.tex
+++ b/doc/refman/RefMan-coi.tex
@@ -5,7 +5,7 @@
 %\begin{document}
 
 %\coverpage{Co-inductive types in Coq}{Eduardo Gim\'enez}
-\chapter[Co-inductive types in Coq]{Co-inductive types in Coq\label{Coinductives}}
+\chapter[Co-inductive types in Coq]{Co-inductive types in Coq\label{Co-inductives}}
 
 %\begin{abstract}
 {\it Co-inductive} types are types whose elements may not be well-founded.
@@ -59,7 +59,7 @@ CoInductive Stream (A:Set) : Set :=
 The syntax of this command is the same as the 
 command \verb!Inductive! (cf. section
 \ref{gal_Inductive_Definitions}).
-Definition of mutually coinductive types are possible.
+Definition of mutually co-inductive types are possible.
 
 As was already said, there are not principles of 
 induction for co-inductive sets, the only way of eliminating these
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 45f0dce21..a9feb34c5 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1584,11 +1584,11 @@ These commands are synonyms of \texttt{Theorem {\ident} \zeroone{\binders} : {\t
 
 This command is useful for theorems that are proved by simultaneous
 induction over a mutually inductive assumption, or that assert mutually
-dependent statements in some mutual coinductive type. It is equivalent
+dependent statements in some mutual co-inductive type. It is equivalent
 to {\tt Fixpoint} or {\tt CoFixpoint}
 (see Section~\ref{CoFixpoint}) but using tactics to build the proof of
 the statements (or the body of the specification, depending on the
-point of view). The inductive or coinductive types on which the
+point of view). The inductive or co-inductive types on which the
 induction or coinduction has to be done is assumed to be non ambiguous
 and is guessed by the system. 
 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index a3713eb36..d1e225636 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -369,7 +369,7 @@ reserved. Hence their precedence and associativity cannot be changed.
 \comindex{CoFixpoint {\ldots} where {\ldots}}
 \comindex{Inductive {\ldots} where {\ldots}}}
 
-Thanks to reserved notations, the inductive, coinductive, recursive
+Thanks to reserved notations, the inductive, co-inductive, recursive
 and corecursive definitions can benefit of customized notations. To do
 this, insert a {\tt where} notation clause after the definition of the
 (co)inductive type or (co)recursive term (or after the definition of
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ca5be4d98..ff85b629b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -921,7 +921,7 @@ system tries to guess itself what they are).
 This tactic starts a proof by coinduction. The identifier {\ident} is
 the name given to the coinduction hypothesis.  Like in a {\tt cofix}
 expression, the use of induction hypotheses have to guarded by a
-constructor.  The verification that the use of coinductive hypotheses
+constructor.  The verification that the use of co-inductive hypotheses
 is correct is done only at the time of registering the lemma in the
 environment. To know if the use of coinduction hypotheses is correct
 at some time of the interactive development of a proof, use the
@@ -1692,7 +1692,7 @@ equivalent to {\tt intros; apply ci}.
 \label{Tac-induction}}
 
 The tactics presented in this section implement induction or case
-analysis on inductive or coinductive objects (see
+analysis on inductive or co-inductive objects (see
 Section~\ref{Cic-inductive-definitions}).
 
 \subsection{\tt induction \term
@@ -1914,16 +1914,16 @@ instantiate premises of the type of {\term$_2$}.
 \label{destruct}
 
 This tactic applies to any goal. The argument {\term} must be of
-inductive or coinductive type and the tactic generates subgoals, one
+inductive or co-inductive type and the tactic generates subgoals, one
 for each possible form of {\term}, i.e. one for each constructor of
-the inductive or coinductive type. Unlike {\tt induction}, no
+the inductive or co-inductive type. Unlike {\tt induction}, no
 induction hypothesis is generated by {\tt destruct}.
 
 If the argument is dependent in either the conclusion or some
 hypotheses of the goal, the argument is replaced by the appropriate
 constructor form in each of the resulting subgoals, thus performing
 case analysis. If non dependent, the tactic simply exposes the
-inductive or coinductive structure of the argument.
+inductive or co-inductive structure of the argument.
 
 There are special cases: