diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdep_lexer.mll | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 4cb5e00879..dfcd22f574 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -50,6 +50,9 @@ let syntax_error lexbuf = raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf)) + (** This is the prefix that should be pre-prepended to files due to the use + ** of [From], i.e. [From Xxx... Require ...] + **) let from_pre_ident = ref None } |