From 86d5ed1d96a93c074a070c86b1c3c81088e4cd2d Mon Sep 17 00:00:00 2001
From: Thomas Letan
Date: Sat, 27 Jul 2019 13:26:17 +0200
Subject: 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.
---
 doc/sphinx/using/tools/coqdoc.rst | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

(limited to 'doc/sphinx/using')

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
 ~~~~~
-- 
cgit v1.2.3