3 files changed, 58 insertions, 4 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 381f8bb661..835d6dcaa6 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -533,10 +533,10 @@ Convertibility
 Let us write :math:`E[Γ] ⊢ t \triangleright u` for the contextual closure of the
 relation :math:`t` reduces to :math:`u` in the global environment
 :math:`E` and local context :math:`Γ` with one of the previous
-reductions β, ι, δ or ζ.
+reductions β, δ, ι or ζ.
 
 We say that two terms :math:`t_1` and :math:`t_2` are
-*βιδζη-convertible*, or simply *convertible*, or *equivalent*, in the
+*βδιζη-convertible*, or simply *convertible*, or *equivalent*, in the
 global environment :math:`E` and local context :math:`Γ` iff there
 exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright
 … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 8c82526f0c..1a33a9a46e 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1112,6 +1112,59 @@ co-inductive definitions are also allowed.
    object of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite
    objects in Section :ref:`cofixpoint`.
 
+Caveat
+++++++
+
+The ability to define co-inductive types by constructors, hereafter called
+*positive co-inductive types*, is known to break subject reduction. The story is
+a bit long: this is due to dependent pattern-matching which implies
+propositional η-equality, which itself would require full η-conversion for
+subject reduction to hold, but full η-conversion is not acceptable as it would
+make type-checking undecidable.
+
+Since the introduction of primitive records in Coq 8.5, an alternative
+presentation is available, called *negative co-inductive types*. This consists
+in defining a co-inductive type as a primitive record type through its
+projections. Such a technique is akin to the *co-pattern* style that can be
+found in e.g. Agda, and preserves subject reduction.
+
+The above example can be rewritten in the following way.
+
+.. coqtop:: all
+
+   Set Primitive Projections.
+   CoInductive Stream : Set := Seq { hd : nat; tl : Stream }.
+   CoInductive EqSt (s1 s2: Stream) : Prop := eqst {
+     eqst_hd : hd s1 = hd s2;
+     eqst_tl : EqSt (tl s1) (tl s2);
+   }.
+
+Some properties that hold over positive streams are lost when going to the
+negative presentation, typically when they imply equality over streams.
+For instance, propositional η-equality is lost when going to the negative
+presentation. It is nonetheless logically consistent to recover it through an
+axiom.
+
+.. coqtop:: all
+
+   Axiom Stream_eta : forall s: Stream, s = cons (hs s) (tl s).
+
+More generally, as in the case of positive coinductive types, it is consistent
+to further identify extensional equality of coinductive types with propositional
+equality:
+
+.. coqtop:: all
+
+   Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2.
+
+As of Coq 8.9, it is now advised to use negative co-inductive types rather than
+their positive counterparts.
+
+.. seealso::
+   :ref:`primitive_projections` for more information about negative
+   records and primitive projections.
+
+
 Definition of recursive functions
 ---------------------------------
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index c802f44ac1..741f9fe5b0 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -144,8 +144,9 @@ list of assertion commands is given in :ref:`Assertions`. The command
    the proof is a subset of the declared one.
 
    The set of declared variables is closed under type dependency. For
-   example if ``T`` is variable and a is a variable of type ``T``, the commands
-   ``Proof using a`` and ``Proof using T a`` are actually equivalent.
+   example, if ``T`` is a variable and ``a`` is a variable of type
+   ``T``, then the commands ``Proof using a`` and ``Proof using T a``
+   are equivalent.
 
    .. cmdv:: Proof using {+ @ident } with @tactic