Further documentation improvements.

1 files changed, 18 insertions, 9 deletions

diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index c1b793b03e..b19239ed22 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -7,6 +7,9 @@ SProp (proof irrelevant propositions)
 
    The status of strict propositions is experimental.
 
+   In particular, conversion checking through bytecode or native code
+   compilation currently does not understand proof irrelevance.
+
 This section describes the extension of |Coq| with definitionally
 proof irrelevant propositions (types in the sort :math:`\SProp`, also
 known as strict propositions) as described in
@@ -34,29 +37,35 @@ Basic constructs
 The purpose of :math:`\SProp` is to provide types where all elements
 are convertible:
 
-.. coqdoc::
+.. coqtop:: all
 
-   Definition irrelevance (A:SProp) (P:A -> Prop) (x:A) (v:P x) (y:A) : P y := v.
+   Theorem irrelevance (A : SProp) (P : A -> Prop) : forall x : A, P x -> forall y : A, P y.
+   Proof.
+   intros * Hx *.
+   exact Hx.
+   Qed.
 
 Since we have definitional :ref:`eta-expansion` for
 functions, the property of being a type of definitionally irrelevant
 values is impredicative, and so is :math:`\SProp`:
 
-.. coqdoc::
+.. coqtop:: all
 
    Check fun (A:Type) (B:A -> SProp) => (forall x:A, B x) : SProp.
 
-.. warning::
-
-   Conversion checking through bytecode or native code compilation
-   currently does not understand proof irrelevance.
-
 In order to keep conversion tractable, cumulativity for :math:`\SProp`
-is forbidden:
+is forbidden, unless the :flag:`Cumulative StrictProp` flag is turned
+on:
 
 .. coqtop:: all
 
    Fail Check (fun (A:SProp) => A : Type).
+   Set Cumulative StrictProp.
+   Check (fun (A:SProp) => A : Type).
+
+.. coqtop:: none
+
+   Unset Cumulative StrictProp.
 
 We can explicitly lift strict propositions into the relevant world by
 using a wrapping inductive type. The inductive stops definitional