diff options
Diffstat (limited to 'plugins/ltac/g_ltac.ml4')
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index fd33a779d..ece0adb07 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -12,7 +12,6 @@ DECLARE PLUGIN "ltac_plugin" open Util open Pp -open Compat open Constrexpr open Tacexpr open Misctypes @@ -68,9 +67,9 @@ let _ = let test_bracket_ident = Gram.Entry.of_parser "test_bracket_ident" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "[" -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | IDENT _ -> () | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) |