diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-23 17:10:41 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-23 17:10:41 +0200 |
| commit | 42dc32440b4b30d05e3f83d24031bc7b207149d6 (patch) | |
| tree | 15871fee3601513f84e4d3849bcccce7f6f64af1 /tools | |
| parent | f5a746eca3866b4652ead49548d08b2fe460960c (diff) | |
| parent | db601b06b0880f573b6d1fa83de471679ce87ee7 (diff) | |
Merge PR#794: Cleanup of ltac cmxs
Diffstat (limited to 'tools')
| -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 } |