1 files changed, 22 insertions, 0 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 862715753d..dd1b65d294 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -469,6 +469,11 @@ module Latex = struct
 
   let stop_emph () = printf "}"
 
+  let start_details _ = ()
+
+  let stop_details () = ()
+
+
   let start_comment () = printf "\\begin{coqdoccomment}\n"
 
   let end_comment () = printf "\\end{coqdoccomment}\n"
@@ -740,6 +745,12 @@ module Html = struct
 
   let stop_emph () = printf "</i>"
 
+  let start_details = function
+    | Some s -> printf "<details><summary>%s</summary>" s
+    | _ -> printf "<details>"
+
+  let stop_details () = printf "</details>"
+
   let start_comment () = printf "<span class=\"comment\">(*"
 
   let end_comment () = printf "*)</span>"
@@ -1053,6 +1064,9 @@ module TeXmacs = struct
   let start_emph () = printf "<with|font shape|italic|"
   let stop_emph () = printf ">"
 
+  let start_details _ = ()
+  let stop_details () = ()
+
   let start_comment () = ()
   let end_comment () = ()
 
@@ -1159,6 +1173,9 @@ module Raw = struct
   let start_emph () = printf "_"
   let stop_emph () = printf "_"
 
+  let start_details _ = ()
+  let stop_details () = ()
+
   let start_comment () = printf "(*"
   let end_comment () = printf "*)"
 
@@ -1272,6 +1289,11 @@ let start_emph =
 let stop_emph =
   select Latex.stop_emph Html.stop_emph TeXmacs.stop_emph Raw.stop_emph
 
+let start_details =
+  select Latex.start_details Html.start_details TeXmacs.start_details Raw.start_details
+let stop_details =
+  select Latex.stop_details Html.stop_details TeXmacs.stop_details Raw.stop_details
+
 let start_latex_math =
   select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math
 let stop_latex_math =