1 files changed, 6 insertions, 7 deletions
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index 6611eba55b..901e686315 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -17,13 +17,12 @@ open Univ
 open Term
 open Environ
 
-let lexer = {
-  Token.func = Lexer.func;
-  Token.using = (function ("",s) -> Lexer.add_keyword s | _ -> ());
-  Token.removing = (fun _ -> ());
-  Token.tparse = Lexer.tparse;
-  Token.text = Lexer.token_text }
-  
+let lexer =
+  {Token.func = Lexer.func; Token.using = Lexer.add_token;
+   Token.removing = (fun _ -> ()); Token.tparse = Lexer.tparse;
+   Token.text = Lexer.token_text}
+;;
+
 type command =
   | Definition of identifier * constr option * constr
   | Parameter of identifier * constr