From 149fefe4802708eacc5f85d39f177bbe8ad4feca Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Jun 2016 11:01:20 -0700 Subject: [PATCH] chore(frontends/lean/token_table): remove 'note' 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 dd06778fc0..550539cf08 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -97,7 +97,7 @@ void init_token_table(token_table & t) { {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0}, {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"xrewrite", 0}, {"krewrite", 0}, - {"esimp", 0}, {"note", 0}, {"with_options", 0}, {"with_attributes", 0}, {"with_attrs", 0}, + {"esimp", 0}, {"with_options", 0}, {"with_attributes", 0}, {"with_attrs", 0}, {"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"#tactic", 0}, {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec}, {"@@", g_max_prec}, {"@", g_max_prec},