diff options
| author | Enrico Tassi | 2019-03-05 11:42:17 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-03-31 14:36:28 +0200 |
| commit | 912eaf40d4efd29b7e3489d51c55b8b79206df79 (patch) | |
| tree | b4793da97a5513d460c3d08721cb40692eeddd71 /parsing/cLexer.mli | |
| parent | ed996432fd079583afbb1797c92ad23f654b94eb (diff) | |
[parsing] Split Tok.t into Tok.t and Tok.pattern
Tokens were having a double role:
- the output of the lexer
- the items of grammar entries, especially terminals
Now tokens are the output of the lexer, and this paves the way for
using a richer data type, eg including Loc.t
Patterns, as in Plexing.pattern, only represent patterns (for tokens)
and now have a bit more structure (eg the wildcard is represented
as None, not as "", while a regular pattern for "x" as Some "x")
Diffstat (limited to 'parsing/cLexer.mli')
| -rw-r--r-- | parsing/cLexer.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 807f37a1a4..662f6a477d 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -21,7 +21,7 @@ val get_keyword_state : unit -> keyword_state val check_ident : string -> unit val is_ident : string -> bool val check_keyword : string -> unit -val terminal : string -> Tok.t +val terminal : string -> Tok.pattern (** The lexer of Coq: *) |