diff options
author | Gregory Malecha <gmalecha@cs.harvard.edu> | 2014-08-01 21:31:39 -0400 |
---|---|---|
committer | Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> | 2014-08-25 14:13:24 +0200 |
commit | 92fcd2cff2b1b0d289b98d14668484b338c8530a (patch) | |
tree | 59d446bf22a59800152e3f960fca0df1d572d63e | |
parent | b45474e03dbba3687db4c7452432e686c32f60a4 (diff) |
a comment about the new state.
-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 4cb5e0087..dfcd22f57 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 } |