From dd198266ff91f619213e0160961b96f2654c59d6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 19 Nov 2018 03:19:45 +0100
Subject: [gramlib] Remove unused alias.

No effect on actual code.
---
 vernac/pvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

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
 
-- 
cgit v1.2.3