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.

2 files changed, 26 insertions, 0 deletions

diff --git a/doc/changelog/08-tools/10592-coqdoc-details.rst b/doc/changelog/08-tools/10592-coqdoc-details.rst
new file mode 100644
index 0000000000..c5bdc1dbb0
--- /dev/null
+++ b/doc/changelog/08-tools/10592-coqdoc-details.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  A new documentation environment ``details`` to make certain portion
+  of a Coq document foldable.  See :ref:`coqdoc`
+  (`#10592 <https://github.com/coq/coq/pull/10592>`_,
+  by Thomas Letan).
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
 ~~~~~