diff options
| -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) |