diff options
| author | Pierre Roux | 2019-01-27 16:01:31 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-04-04 23:44:00 +0200 |
| commit | 0d8a4ec0f7486f47b7cff4cda465e2bd10c163ac (patch) | |
| tree | 8834c79b4efe2f2ccb516828956349ec2cb89f7d | |
| parent | dc903c82c2308ae638147c5428511abe9279bf6d (diff) | |
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) |