aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gregory Malecha <gmalecha@cs.harvard.edu>2014-08-01 21:31:39 -0400
committerGravatar Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr>2014-08-25 14:13:24 +0200
commit92fcd2cff2b1b0d289b98d14668484b338c8530a (patch)
tree59d446bf22a59800152e3f960fca0df1d572d63e
parentb45474e03dbba3687db4c7452432e686c32f60a4 (diff)
a comment about the new state.
-rw-r--r--tools/coqdep_lexer.mll3
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
}