coqdoc: Add (* begin details *) and (* end details *)

We propose to add an environment to have foldable texts with HTML
output, more precisely:

    (*begin details [: An optional summary] *)

    some Coq and documentation material

    (* end details *)

Currently, only the HTML output is supported. We could treat this
environment in LaTeX output as appendixes to output later.

1 files changed, 21 insertions, 0 deletions

diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst
index cada680895..b4b14fb392 100644
--- a/doc/sphinx/using/tools/coqdoc.rst
+++ b/doc/sphinx/using/tools/coqdoc.rst
@@ -248,6 +248,27 @@ shown using such comments:
 The latter cannot be used around some inner parts of a proof, but can
 be used around a whole proof.
 
+Lastly, it is possible to adopt a middle-ground approach when the
+desired output is HTML, where a given snippet of Coq material is
+hidden by default, but can be made visible with user interaction.
+
+::
+
+
+    (* begin details *)
+     *some Coq material*
+    (* end details *)
+
+
+There is also an alternative syntax available.
+
+::
+
+
+    (* begin details : Some summary describing the snippet *)
+     *some Coq material*
+    (* end details *)
+
 
 Usage
 ~~~~~