From b221b09ad5308604246e778dcb22fef3b2850c63 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 31 Jul 2019 17:07:05 -0700
Subject: [PATCH] chore(library/init, frontends/lean): ensure old and new
 parser use the same command for initializing quotient module

---
 lean4-mode/lean4-syntax.el          | 2 +-
 library/init/core.lean              | 2 +-
 src/frontends/lean/builtin_cmds.cpp | 2 +-
 src/frontends/lean/token_table.cpp  | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/lean4-mode/lean4-syntax.el b/lean4-mode/lean4-syntax.el
index 249dcde17c..df9436e652 100644
--- a/lean4-mode/lean4-syntax.el
+++ b/lean4-mode/lean4-syntax.el
@@ -19,7 +19,7 @@
     "attribute" "local" "set_option" "extends" "include" "omit" "classes" "class"
     "attributes" "raw" "replacing"
     "calc" "have" "show" "suffices" "by" "in" "at" "do" "let" "forall" "Pi" "fun"
-    "exists" "if" "then" "else" "assume" "from"
+    "exists" "if" "then" "else" "assume" "from" "init_quot"
     "mutual" "def" "run_cmd")
   "lean keywords ending with 'word' (not symbol)")
 (defconst lean4-keywords1-regexp
diff --git a/library/init/core.lean b/library/init/core.lean
index 096db8bd01..a93a0f9742 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -203,7 +203,7 @@ constant Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α
 constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
   (∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q
 -/
-initQuot
+init_quot
 
 inductive Heq {α : Sort u} (a : α) : ∀ {β : Sort u}, β → Prop
 | refl : Heq a
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 3d2729f18a..447a12950a 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -407,7 +407,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("namespace",         "open a new namespace", namespace_cmd));
     add_cmd(r, cmd_info("end",               "close the current namespace/section", end_scoped_cmd));
     add_cmd(r, cmd_info("#check",            "type check given expression, and display its type", check_cmd));
-    add_cmd(r, cmd_info("initQuot",          "initialize `quot` type computational rules", init_quot_cmd));
+    add_cmd(r, cmd_info("init_quot",         "initialize `quot` type computational rules", init_quot_cmd));
     add_cmd(r, cmd_info("import",            "import module(s)", import_cmd));
     add_cmd(r, cmd_info("hide",              "hide aliases in the current scope", hide_cmd));
     register_decl_cmds(r);
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 849be5a3f4..b618d4a01c 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -106,7 +106,7 @@ void init_token_table(token_table & t) {
          "import", "inductive", "coinductive", "structure", "class", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
          "set_option", "open", "export", "@[",
-         "attribute", "instance", "include", "omit", "initQuot",
+         "attribute", "instance", "include", "omit", "init_quot",
          "run_cmd", "#check", "#reduce", "#eval", "#print", "#help", "#exit",
          "#compile", "#unify", "#compact_tst", nullptr};