From 73ed9db1617faed868ef712acebada84bdf84d42 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Oct 2016 08:46:23 -0700 Subject: [PATCH] chore(frontends/lean/token_table): remove old keyword --- src/frontends/lean/token_table.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 8dbda875b3..9c246a7dba 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -89,7 +89,7 @@ void init_token_table(token_table & t) { {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0}, {"//", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"without", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0}, - {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec}, {"using", 0}, + {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"using", 0}, {"@@", g_max_prec}, {"@", g_max_prec}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0}, {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},