From 2a596b2f6df4d884aaec99a519044036a4a81596 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 9 Jul 2009 14:40:57 +0000
Subject: Allow coqdoc comments inside definition bodies.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12237 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tools/coqdoc/cpretty.mll | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'tools')

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index bda18e03ca..5ca970f353 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 
-- 
cgit v1.2.3