From 1d62a614e78eac81c4e5431655ef26ace3027122 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Jul 2014 15:05:44 -0700 Subject: [PATCH] fix(frontends/lean): remove keywords 'class' and '[class]' Signed-off-by: Leonardo de Moura --- src/frontends/lean/token_table.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 385662c42..b00dfe475 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -73,12 +73,12 @@ token_table init_token_table() { {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}}; char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion", - "variables", "[private]", "[inline]", "[fact]", "[instance]", "[class]", "[module]", "[coercion]", + "variables", "[private]", "[inline]", "[fact]", "[instance]", "[module]", "[coercion]", "abbreviation", "opaque_hint", "evaluate", "check", "print", "end", "namespace", "section", "import", "abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe", "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "exit", "set_option", "using", "calc_subst", "calc_refl", "calc_trans", "tactic_hint", - "add_proof_qed", "set_proof_qed", "#setline", "class", "instance", nullptr}; + "add_proof_qed", "set_proof_qed", "#setline", "instance", nullptr}; std::pair aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},