diff --git a/src/frontends/lean/parse_table.h b/src/frontends/lean/parse_table.h index fd2a8f311..441d0cf75 100644 --- a/src/frontends/lean/parse_table.h +++ b/src/frontends/lean/parse_table.h @@ -118,5 +118,6 @@ public: void for_each(std::function const &)> const & fn) const; }; } +typedef notation::parse_table parse_table; void open_parse_table(lua_State * L); }