Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

1 files changed, 2 insertions, 2 deletions

diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex
index 619a8ee1..e609fce8 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