diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-30 16:47:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-30 16:49:15 +0200 |
| commit | 72f128af5a00e5509239e46b395c9cd10e53b36a (patch) | |
| tree | f0b9aecae361704b534abf45ebc63a1cabd5c3fb /tools/coqdep_lexer.mli | |
| parent | 2defd4c15467736b73f69adb501e3a4fe2111ce5 (diff) | |
Removing dead code in coqdep.
Since commit 2f521670fbd, the Require "file" syntax was not used anymore by
coqtop but the code handling it was still there in coqdep. We finish the work
by erasing the remnant code.
Diffstat (limited to 'tools/coqdep_lexer.mli')
| -rw-r--r-- | tools/coqdep_lexer.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli index b447030af..c7b9c9a0a 100644 --- a/tools/coqdep_lexer.mli +++ b/tools/coqdep_lexer.mli @@ -12,7 +12,6 @@ type qualid = string list type coq_token = Require of qualid list - | RequireString of string | Declare of string list | Load of string | AddLoadPath of string |