diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 574e22d50e..90dda4850e 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -72,7 +72,7 @@ let test_lpar_idnum_coloneq = match stream_nth 0 strm with | KEYWORD "(" -> (match stream_nth 1 strm with - | IDENT _ | INT _ -> + | IDENT _ | NUMERAL _ -> (match stream_nth 2 strm with | KEYWORD ":=" -> () | _ -> err ()) |