aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep_lexer.mll
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdep_lexer.mll')
-rwxr-xr-xtools/coqdep_lexer.mll2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index b13c16bad..89eeed54a 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -55,7 +55,7 @@ rule coq_action = parse
{ module_names := []; opened_file lexbuf}
| "Require" space+ "Import" space+
{ module_names := []; opened_file lexbuf}
- | "Declare" space+ "ML" space+ "Module" space+
+ | "Local"? "Declare" space+ "ML" space+ "Module" space+
{ mllist := []; modules lexbuf}
| "Load" space+
{ load_file lexbuf }