Add support for Local Declare ML Module

Instead of failing with some obscure error message *after* loading the
module, accept Local Declare ML Module with the usual semantics.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12366 85f007b7-540e-0410-9357-904b9bb8a0f7

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 }