diff options
| author | Pierre-Marie Pédrot | 2019-04-05 09:40:46 +0200 |
|---|---|---|
| committer | GitHub | 2019-04-05 09:40:46 +0200 |
| commit | d47892548aebfb6640a8721ee1ec3493bfd3ce2a (patch) | |
| tree | 8834c79b4efe2f2ccb516828956349ec2cb89f7d | |
| parent | dc903c82c2308ae638147c5428511abe9279bf6d (diff) | |
| parent | 0d8a4ec0f7486f47b7cff4cda465e2bd10c163ac (diff) | |
Merge pull request coq/ltac2#116 from proux01/master-parsing-decimal
[coq] Adapt to coq/coq#8764
| -rw-r--r-- | src/g_ltac2.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/g_ltac2.mlg b/src/g_ltac2.mlg index fcf5d59ec9..0071dbb088 100644 --- a/src/g_ltac2.mlg +++ b/src/g_ltac2.mlg @@ -44,7 +44,7 @@ let lk_ident n strm = match stream_nth n strm with | _ -> None let lk_int n strm = match stream_nth n strm with -| INT _ -> Some (n + 1) +| NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1) | _ -> None let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident) |