From 31c7542731a62f56bd60f443a84d68813f8780a8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 30 Jun 2015 16:39:54 +0200
Subject: Fixing bug #4265: coqdep does not handle From ... Require.

The search algorithm is not satisfactory though, as it crawls through
all known files to find the proper one. We should rather use some trie-based
data structure, but I'll leave this for a future commit.
---
 tools/coqdep_lexer.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools/coqdep_lexer.mli')

diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli
index c7b9c9a0a..84c9ba798 100644
--- a/tools/coqdep_lexer.mli
+++ b/tools/coqdep_lexer.mli
@@ -11,7 +11,7 @@ type mL_token = Use_module of string
 type qualid = string list
 
 type coq_token =
-    Require of qualid list
+    Require of qualid option * qualid list
   | Declare of string list
   | Load of string
   | AddLoadPath of string
-- 
cgit v1.2.3