From feb92894c6be249abadd3303cfca3b258d6f3ea8 Mon Sep 17 00:00:00 2001
From: glondu
Date: Tue, 29 Sep 2009 15:11:52 +0000
Subject: 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
---
 tools/coqdep_lexer.mll | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index b13c16bad9..89eeed54ab 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 }
-- 
cgit v1.2.3