diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-15 10:13:37 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-15 10:13:53 +0200 |
| commit | 48219205d121ea3093287ac1b887fc81067fac6a (patch) | |
| tree | 950c59fac8113d5097efe5b235ef042e504af61e /tools/coqdep_lexer.mll | |
| parent | e1d68573015883301cb401861e10233f6442d9ec (diff) | |
coqdep: correct support of Local Declare ML Module
Diffstat (limited to 'tools/coqdep_lexer.mll')
| -rw-r--r-- | tools/coqdep_lexer.mll | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index c68c34bbb..9224cdafe 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 } |