aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdep_lexer.mll4
1 files changed, 3 insertions, 1 deletions
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index c68c34bbbd..9224cdafe8 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -74,7 +74,9 @@ let dot = '.' ( space+ | eof)
rule coq_action = parse
| "Require" space+
{ require_modifiers None lexbuf }
- | "Local"? "Declare" space+ "ML" space+ "Module" space+
+ | "Local" space+ "Declare" space+ "ML" space+ "Module" space+
+ { modules [] lexbuf }
+ | "Declare" space+ "ML" space+ "Module" space+
{ modules [] lexbuf }
| "Load" space+
{ load_file lexbuf }