From 69784189812fce435dbb688b02c3343ddda03a93 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 3 Jun 2016 09:11:47 +0200
Subject: Fix proof terminators not being detected in presence of curly
 brackets (bug #4770).

This also fixes comments not being properly skipped when looking for eol.
---
 tools/coqdoc/cpretty.mll | 24 +++++++++++++++++++++---
 1 file changed, 21 insertions(+), 3 deletions(-)

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 7bc342555e..9191b2acac 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -557,7 +557,7 @@ rule coq_bol = parse
 	  if not !Cdglobals.gallina then
 	    begin backtrack lexbuf; body_bol lexbuf end
 	  else
-	    skip_to_dot lexbuf
+	    skip_to_dot_or_brace lexbuf
 	in
 	  if eol then coq_bol lexbuf else coq lexbuf }
 
@@ -653,7 +653,7 @@ and coq = parse
 	  if not !Cdglobals.gallina then
 	    begin backtrack lexbuf; body lexbuf end
 	  else
-	    skip_to_dot lexbuf
+	    skip_to_dot_or_brace lexbuf
 	in
 	  if eol then coq_bol lexbuf else coq lexbuf}
 
@@ -1063,7 +1063,25 @@ and comment = parse
 and skip_to_dot = parse
   | '.' space* nl { true }
   | eof | '.' space+ { false }
-  | "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
+  | "(*"
+      { comment_level := 1;
+        ignore (skipped_comment lexbuf);
+        skip_to_dot lexbuf }
+  | _ { skip_to_dot lexbuf }
+
+and skip_to_dot_or_brace = parse
+  | '.' space* nl { true }
+  | eof | '.' space+ { false }
+  | "(*"
+      { comment_level := 1;
+        ignore (skipped_comment lexbuf);
+        skip_to_dot_or_brace lexbuf }
+  | "}" space* nl
+      { true }
+  | "}"
+      { false }
+  | space*
+      { skip_to_dot_or_brace lexbuf }
   | _ { skip_to_dot lexbuf }
 
 and body_bol = parse
-- 
cgit v1.2.3