Allow coqdoc comments inside definition bodies.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12237 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 0 deletions

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index bda18e03c..5ca970f35 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -718,6 +718,11 @@ and body = parse
   | '.' space+ { Output.char '.'; Output.char ' '; 
 	  if not !formatted then false else body lexbuf }
   | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
+  | "(**" space_nl
+      { Output.end_coq (); Output.start_doc (); 
+	let eol = doc_bol lexbuf in
+	  Output.end_doc (); Output.start_coq (); 
+	  if eol then body_bol lexbuf else body lexbuf }
   | "(*" { comment_level := 1; 
 	   if !Cdglobals.parse_comments then Output.start_comment ();
 	   let eol = comment lexbuf in