diff options
| author | Emilio Jesus Gallego Arias | 2020-02-21 14:18:37 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:01 -0400 |
| commit | ef3079e22fa7941d3335d7779c840e8d2d2bde39 (patch) | |
| tree | 6f524c811c79c1e3271b2c86ce3b29275b876075 /parsing | |
| parent | 9847448b5f9dbf32806decf676f415d584a2cddb (diff) | |
[parsing] Move comments lexer extensions to base lexer interface
This makes sense as a step towards a more functional handling of the
state.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/cLexer.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 67b8310bde..ac2c5bcfe2 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -55,7 +55,7 @@ val terminal_numeral : string -> NumTok.Unsigned.t Tok.p (** The lexer of Coq: *) module Lexer : - Gramlib.Grammar.GLexerType with type te = Tok.t and type 'c pattern = 'c Tok.p + Gramlib.Plexing.S with type te = Tok.t and type 'c pattern = 'c Tok.p module Error : sig type t @@ -74,4 +74,4 @@ it was not in a comment, possibly becoming multiple tokens *) module LexerDiff : - Gramlib.Grammar.GLexerType with type te = Tok.t and type 'c pattern = 'c Tok.p + Gramlib.Plexing.S with type te = Tok.t and type 'c pattern = 'c Tok.p |