From 9bef662f678dfbeaa477b6d336a4bd141d102b91 Mon Sep 17 00:00:00 2001
From: Gregory Malecha
Date: Thu, 7 Aug 2014 09:00:40 -0400
Subject: factored out require_modifiers + bug fix.

Conflicts:
	tools/coqdep_lexer.mll
---
 tools/coqdep_lexer.mll | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index aadced8b05..025b94d44a 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -82,11 +82,7 @@ let dot = '.' ( space+ | eof)
 
 rule coq_action = parse
   | "Require" space+
-      { require_file lexbuf }
-  | "Require" space+ "Export" space+
-      { require_file lexbuf }
-  | "Require" space+ "Import" space+
-      { require_file lexbuf }
+      { require_modifiers lexbuf }
   | "Local"? "Declare" space+ "ML" space+ "Module" space+
       { mllist := []; modules lexbuf }
   | "Load" space+
@@ -123,13 +119,27 @@ and from_rule = parse
   | _
       { syntax_error lexbuf }
 
+and require_modifiers = parse
+  | "(*"
+      { comment lexbuf; require_modifiers lexbuf }
+  | "Import" space+
+      { require_file lexbuf }
+  | "Export" space+
+      { require_file lexbuf }
+  | space+
+      { require_modifiers lexbuf }
+  | eof
+      { syntax_error lexbuf }
+  | _
+      { backtrack lexbuf ; require_file lexbuf }
+
 and consume_require = parse
   | "(*"
       { comment lexbuf; consume_require lexbuf }
   | space+
       { consume_require lexbuf }
   | "Require" space+
-      { require_file lexbuf }
+      { require_modifiers lexbuf }
   | eof
       { syntax_error lexbuf }
   | _
-- 
cgit v1.2.3