diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-02 16:09:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-02 19:59:09 +0200 |
| commit | 5b70748b082b9ca33c72d62e076b61ed1e073b8a (patch) | |
| tree | d03b621566ec7658021554f5f56d3b786b0d896b /grammar/coqpp_lex.mll | |
| parent | 02fe76c0c1c3f01c6fb4310dd4450b35f43005da (diff) | |
Implementing TACTIC EXTEND in coqpp.
Diffstat (limited to 'grammar/coqpp_lex.mll')
| -rw-r--r-- | grammar/coqpp_lex.mll | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/grammar/coqpp_lex.mll b/grammar/coqpp_lex.mll index f35766b16..6c6562c20 100644 --- a/grammar/coqpp_lex.mll +++ b/grammar/coqpp_lex.mll @@ -83,6 +83,7 @@ let alphanum = ['_' 'a'-'z' 'A'-'Z' '0'-'9' '\''] let ident = letterlike alphanum* let qualid = ident ('.' ident)* let space = [' ' '\t' '\r'] +let number = [ '0'-'9' ] rule extend = parse | "(*" { start_comment (); comment lexbuf } @@ -92,6 +93,8 @@ rule extend = parse | "TACTIC" { TACTIC } | "EXTEND" { EXTEND } | "END" { END } +| "DECLARE" { DECLARE } +| "PLUGIN" { PLUGIN } (** Camlp5 specific keywords *) | "GLOBAL" { GLOBAL } | "FIRST" { FIRST } @@ -105,6 +108,7 @@ rule extend = parse (** Standard *) | ident { IDENT (Lexing.lexeme lexbuf) } | qualid { QUALID (Lexing.lexeme lexbuf) } +| number { INT (int_of_string (Lexing.lexeme lexbuf)) } | space { extend lexbuf } | '\"' { string lexbuf } | '\n' { newline lexbuf; extend lexbuf } |