diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ded7a557c..71b93439b 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Compat open CErrors open Util open Names @@ -407,7 +406,7 @@ let only_starredidentrefs = Gram.Entry.of_parser "test_only_starredidentrefs" (fun strm -> let rec aux n = - match get_tok (Util.stream_nth n strm) with + match Util.stream_nth n strm with | KEYWORD "." -> () | KEYWORD ")" -> () | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1) |