coqdoc: Fix the “details” environment

The change introduced by 41a1d66 has broken the feature prior to its
initial release. We attempt to fix the issue, and add a comment to
warn feature developers in order to avoid facing the same issue again.

1 files changed, 3 insertions, 3 deletions

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index b801a3b06e..5d210b2e60 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -504,9 +504,9 @@ rule coq_bol = parse
       { Lexing.new_line lexbuf; begin_show (); coq_bol lexbuf }
   | space* end_show nl
       { Lexing.new_line lexbuf; end_show (); coq_bol lexbuf }
-  | space* begin_details nl
-      { Lexing.new_line lexbuf;
-        let s = details_body lexbuf in
+  | space* begin_details (* At this point, the comment remains open,
+                            and will be closed by [details_body] *)
+      { let s = details_body lexbuf in
         Output.end_coq (); begin_details s; Output.start_coq (); coq_bol lexbuf }
   | space* end_details nl
       { Lexing.new_line lexbuf;