[gramlib] Remove unused alias.

No effect on actual code.

4 files changed, 2 insertions, 16 deletions

diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 760410894a..1ce0136c1d 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -862,7 +862,6 @@ module type S =
         val parse_token_stream : 'a e -> te Stream.t -> 'a
         val print : Format.formatter -> 'a e -> unit
         external obj : 'a e -> te Gramext.g_entry = "%identity"
-        val parse_token : 'a e -> te Stream.t -> 'a
       end
     type ('self, 'a) ty_symbol
     type ('self, 'f, 'r) ty_rule
@@ -930,18 +929,6 @@ module GMake (L : GLexerType) =
           Obj.magic (parse_parsable e p : Obj.t)
         let parse_token_stream (e : 'a e) ts : 'a =
           Obj.magic (e.estart 0 ts : Obj.t)
-        let _warned_using_parse_token = ref false
-        let parse_token (entry : 'a e) ts : 'a =
-          (* commented: too often warned in Coq...
-          if not warned_using_parse_token.val then do {
-            eprintf "<W> use of Entry.parse_token ";
-            eprintf "deprecated since 2017-06-16\n%!";
-            eprintf "use Entry.parse_token_stream instead\n%! ";
-            warned_using_parse_token.val := True
-          }
-          else ();
-          *)
-          parse_token_stream entry ts
         let name e = e.ename
         let of_parser n (p : te Stream.t -> 'a) : 'a e =
           {egram = gram; ename = n; elocal = false;
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 244ab710dc..1c5fcb7bbf 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -36,7 +36,6 @@ module type S =
         val parse_token_stream : 'a e -> te Stream.t -> 'a
         val print : Format.formatter -> 'a e -> unit
         external obj : 'a e -> te Gramext.g_entry = "%identity"
-        val parse_token : 'a e -> te Stream.t -> 'a
       end
     type ('self, 'a) ty_symbol
     type ('self, 'f, 'r) ty_rule
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index eb3e633892..d4aa598fd8 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -59,7 +59,7 @@ module type S =
         type e 'a = 'y;
         value create : string -> e 'a;
         value parse : e 'a -> parsable -> 'a;
-        value parse_token : e 'a -> Stream.t te -> 'a;
+        value parse_token_stream : e 'a -> Stream.t te -> 'a;
         value name : e 'a -> string;
         value of_parser : string -> (Stream.t te -> 'a) -> e 'a;
         value print : Format.formatter -> e 'a -> unit;
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index b2fa8ec99f..4761e4bbc2 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -42,7 +42,7 @@ module Vernac_ =
     let command_entry_ref = ref noedit_mode
     let command_entry =
       Gram.Entry.of_parser "command_entry"
-        (fun strm -> Gram.Entry.parse_token !command_entry_ref strm)
+        (fun strm -> Gram.Entry.parse_token_stream !command_entry_ref strm)
 
   end