From f177082c3ba4730b0d3ee0397da4054869309497 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Dec 2015 10:30:23 -0800
Subject: [PATCH] refactor(*): normalize metaclass names

@avigad and @fpvandoorn, I changed the metaclasses names. They
were not uniform:
- The plural was used in some cases (e.g., [coercions]).
- In other cases a cryptic name was used (e.g., [brs]).

Now, I tried to use the attribute name as the metaclass name whenever
possible. For example, we write

   definition foo [coercion] ...
   definition bla [forward] ...

and

  open [coercion] nat
  open [forward] nat

It is easier to remember and is uniform.
---
 hott/init/default.hlean                       |  8 +++---
 hott/init/equiv.hlean                         |  4 +--
 hott/init/function.hlean                      |  2 +-
 library/data/bag.lean                         |  2 +-
 library/data/finset/basic.lean                |  2 +-
 library/data/hf.lean                          |  4 +--
 library/data/int/div.lean                     |  4 +--
 library/data/real/basic.lean                  |  2 +-
 library/data/real/complete.lean               |  2 +-
 library/data/real/division.lean               |  2 +-
 library/data/real/order.lean                  |  2 +-
 library/init/function.lean                    |  2 +-
 library/theories/analysis/real_limit.lean     |  2 +-
 src/emacs/lean-syntax.el                      |  8 +++---
 src/frontends/lean/begin_end_ext.cpp          |  4 +--
 src/frontends/lean/builtin_cmds.cpp           | 25 ++++++++++++-------
 src/frontends/lean/parser_config.cpp          |  8 +++---
 src/frontends/lean/tactic_hint.cpp            |  4 +--
 src/frontends/lean/tokens.cpp                 | 16 ++++++------
 src/frontends/lean/tokens.h                   |  4 +--
 src/frontends/lean/tokens.txt                 |  4 +--
 src/library/abbreviation.cpp                  |  4 +--
 src/library/aliases.cpp                       |  2 +-
 .../blast/backward/backward_rule_set.cpp      |  4 +--
 .../blast/grinder/intro_elim_lemmas.cpp       |  2 +-
 .../blast/simplifier/simp_rule_set.cpp        |  4 +--
 src/library/class.cpp                         |  2 +-
 src/library/coercion.cpp                      |  4 +--
 src/library/light_lt_manager.cpp              |  4 +--
 src/library/normalize.cpp                     |  4 +--
 src/library/reducible.cpp                     |  4 +--
 src/library/relation_manager.cpp              |  4 +--
 src/library/user_recursors.cpp                |  2 +-
 tests/lean/bad_open.lean                      |  2 +-
 tests/lean/bad_open.lean.expected.out         |  2 +-
 tests/lean/extra/bag.lean                     |  2 +-
 tests/lean/open_tst.lean                      |  6 ++---
 tests/lean/run/568.lean                       |  8 +++---
 tests/lean/run/blast_simp_sum.lean            |  2 +-
 tests/lean/run/class5.lean                    |  2 +-
 tests/lean/run/e11.lean                       |  8 +++---
 tests/lean/run/e12.lean                       | 18 ++++++-------
 tests/lean/run/e8.lean                        |  8 +++---
 tests/lean/run/ppbeta.lean                    |  4 +--
 tests/lean/t14.lean                           |  4 +--
 45 files changed, 112 insertions(+), 105 deletions(-)

diff --git a/hott/init/default.hlean b/hott/init/default.hlean
index a3f0c0f40..f083de41e 100644
--- a/hott/init/default.hlean
+++ b/hott/init/default.hlean
@@ -17,11 +17,11 @@ namespace core
   export empty (hiding elim)
   export sum (hiding elim)
   export sigma (hiding pr1 pr2)
-  export [notations] prod
-  export [notations] nat
+  export [notation] prod
+  export [notation] nat
   export eq (idp idpath concat inverse transport ap ap10 cast tr_inv homotopy ap11 apd refl)
-  export [declarations] function
+  export [declaration] function
   export equiv (to_inv to_right_inv to_left_inv)
   export is_equiv (inv right_inv left_inv adjointify)
-  export [abbreviations] [declarations] is_trunc (trunctype hprop.mk hset.mk)
+  export [abbreviation] [declaration] is_trunc (trunctype hprop.mk hset.mk)
 end core
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index a1bc4dab2..b54c47a24 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -373,5 +373,5 @@ namespace is_equiv
 
 end is_equiv
 
-export [unfold_hints] equiv
-export [unfold_hints] is_equiv
+export [unfold] equiv
+export [unfold] is_equiv
diff --git a/hott/init/function.hlean b/hott/init/function.hlean
index a6ff7dfda..655ff42b9 100644
--- a/hott/init/function.hlean
+++ b/hott/init/function.hlean
@@ -60,4 +60,4 @@ notation f ` -[` op `]- ` g  := combine f op g
 end function
 
 -- copy reducible annotations to top-level
-export [reduce_hints] [unfold_hints] function
+export [reducible] [unfold] function
diff --git a/library/data/bag.lean b/library/data/bag.lean
index e3a6fa5b4..2e27f39c9 100644
--- a/library/data/bag.lean
+++ b/library/data/bag.lean
@@ -7,7 +7,7 @@ Finite bags.
 -/
 import data.nat data.list.perm algebra.binary
 open nat quot list subtype binary function eq.ops
-open [declarations] perm
+open [decl] perm
 
 variable {A : Type}
 
diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean
index 7a789a321..6bacb0425 100644
--- a/library/data/finset/basic.lean
+++ b/library/data/finset/basic.lean
@@ -7,7 +7,7 @@ Finite sets.
 -/
 import data.fintype.basic data.nat data.list.perm algebra.binary
 open nat quot list subtype binary function eq.ops
-open [declarations] perm
+open [decl] perm
 
 definition nodup_list (A : Type) := {l : list A | nodup l}
 
diff --git a/library/data/hf.lean b/library/data/hf.lean
index d92e3f50d..cc2b7d3e7 100644
--- a/library/data/hf.lean
+++ b/library/data/hf.lean
@@ -11,7 +11,7 @@ this bijection is implemeted using the Ackermann coding.
 -/
 import data.nat data.finset.equiv data.list
 open nat binary
-open - [notations] finset
+open - [notation] finset
 
 definition hf := nat
 
@@ -479,7 +479,7 @@ theorem empty_mem_powerset (s : hf) : ∅ ∈ 𝒫 s :=
 mem_powerset_of_subset (empty_subset s)
 
 /- hf as lists -/
-open - [notations] list
+open - [notation] list
 
 definition of_list (s : list hf) : hf :=
 @equiv.to_fun _ _ list_nat_equiv_nat s
diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index f03705334..9b21a8b40 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -8,8 +8,8 @@ Definitions and properties of div and mod, following the SSReflect library.
 Following SSReflect and the SMTlib standard, we define a % b so that 0 ≤ a % b < |b| when b ≠ 0.
 -/
 import data.int.order data.nat.div
-open [coercions] [reduce_hints] nat
-open [declarations] [classes] nat (succ)
+open [coercion] [reducible] nat
+open [declaration] [class] nat (succ)
 open eq.ops
 
 namespace int
diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index ccf24a353..22cf83401 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -22,7 +22,7 @@ The construction of the reals is arranged in four files.
 -/
 import data.nat data.rat.order data.pnat
 open nat eq pnat
-open - [coercions] rat
+open - [coercion] rat
 
 local postfix `⁻¹` := pnat.inv
 
diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean
index 0ed89c328..15a1b6209 100644
--- a/library/data/real/complete.lean
+++ b/library/data/real/complete.lean
@@ -163,7 +163,7 @@ theorem r_equiv_neg_abs_of_le_zero {s : reg_seq} (Hz : r_le s r_zero) : requiv (
 end rat_seq
 
 namespace real
-open [classes] rat_seq
+open [class] rat_seq
 
 private theorem rewrite_helper9 (a b c : ℝ) : b - c = (b - a) - (c - a) :=
   by rewrite [-sub_add_eq_sub_sub_swap, sub_add_cancel]
diff --git a/library/data/real/division.lean b/library/data/real/division.lean
index f1379c261..0766ccf65 100644
--- a/library/data/real/division.lean
+++ b/library/data/real/division.lean
@@ -581,7 +581,7 @@ theorem r_abs_well_defined {s t : reg_seq} (H : requiv s t) : requiv (r_abs s) (
 end rat_seq
 
 namespace real
-open [classes] rat_seq
+open [class] rat_seq
 
 noncomputable protected definition inv (x : ℝ) : ℝ :=
   quot.lift_on x (λ a, quot.mk (rat_seq.r_inv a))
diff --git a/library/data/real/order.lean b/library/data/real/order.lean
index 57e6976d2..a32d4f2a7 100644
--- a/library/data/real/order.lean
+++ b/library/data/real/order.lean
@@ -1015,7 +1015,7 @@ theorem r_le_of_reprs_le (s t : reg_seq) (Hle : ∀ n : ℕ+, r_le (r_const (reg
 end rat_seq
 
 open real
-open [classes] rat_seq
+open [class] rat_seq
 namespace real
 
 protected definition lt (x y : ℝ) :=
diff --git a/library/init/function.lean b/library/init/function.lean
index d8acd33dd..1110039d0 100644
--- a/library/init/function.lean
+++ b/library/init/function.lean
@@ -156,4 +156,4 @@ theorem bijective_id : bijective (@id A) := and.intro injective_id surjective_id
 end function
 
 -- copy reducible annotations to top-level
-export [reduce_hints] [unfold_hints] function
+export [reducible] [unfold] function
diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean
index 252c20fa1..43ddbfba9 100644
--- a/library/theories/analysis/real_limit.lean
+++ b/library/theories/analysis/real_limit.lean
@@ -38,7 +38,7 @@ protected definition metric_space [instance] : metric_space ℝ :=
 ⦄
 
 open nat
-open [classes] rat
+open [class] rat
 
 definition converges_to_seq (X : ℕ → ℝ) (y : ℝ) : Prop :=
 ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 7b74acbe7..de2147b60 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -54,10 +54,10 @@
          '("persistent" "notation" "visible" "instance" "trans_instance"
            "class" "parsing_only" "coercion" "unfold_full" "constructor"
            "reducible" "irreducible" "semireducible" "quasireducible" "wf"
-           "whnf" "multiple_instances" "none" "decls" "declarations"
-           "coercions" "classes" "symm" "subst" "refl" "trans" "simp" "simps" "congr"
-           "forward" "no_pattern" "notations" "abbreviations" "begin_end_hints" "tactic_hints"
-           "reduce_hints" "unfold_hints" "aliases" "eqv" "intro" "intro!" "elim"
+           "whnf" "multiple_instances" "none" "decl" "declaration"
+           "relation" "symm" "subst" "refl" "trans" "simp" "congr"
+           "backward" "forward" "no_pattern" "begin_end" "tactic" "abbreviation"
+           "reducible" "unfold" "alias" "eqv" "intro" "intro!" "elim" "grinder"
            "localrefinfo" "recursor"))
   "lean modifiers")
 (defconst lean-modifiers-regexp
diff --git a/src/frontends/lean/begin_end_ext.cpp b/src/frontends/lean/begin_end_ext.cpp
index 1a892e557..68645f0f7 100644
--- a/src/frontends/lean/begin_end_ext.cpp
+++ b/src/frontends/lean/begin_end_ext.cpp
@@ -78,8 +78,8 @@ bool is_begin_end_annotation(expr const & e) { return is_annotation(e, *g_begin_
 bool is_begin_end_element_annotation(expr const & e) { return is_annotation(e, *g_begin_end_element); }
 
 void initialize_begin_end_ext() {
-    g_class_name = new name("begin_end_hints");
-    g_key        = new std::string("bepretac");
+    g_class_name = new name("begin_end");
+    g_key        = new std::string("BEPRETAC");
     begin_end_ext::initialize();
     g_begin_end  = new name("begin_end");
     g_begin_end_element = new name("begin_end_element");
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 27380e56e..6a1dc1469 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -221,19 +221,26 @@ static optional<name> parse_metaclass(parser & p) {
             p.next();
         }
         p.check_token_next(get_rbracket_tk(), "invalid 'open' command, ']' expected");
-        if (!is_metaclass(n) && n != get_decls_tk() && n != get_declarations_tk())
+        if (!is_metaclass(n) && n != get_decl_tk() && n != get_declaration_tk())
             throw parser_error(sstream() << "invalid metaclass name '[" << n << "]'", pos);
         return optional<name>(n);
     } else if (p.curr() == scanner::token_kind::CommandKeyword) {
+        // Meta-classes whose name conflict with tokens of the form `[<id>]` `[<id>`
+        // Example: [class] and [unfold
         name v = p.get_token_info().value();
-        if (v.is_atomic() && v.is_string() && v.size() > 2 && v.get_string()[0] == '[' && v.get_string()[v.size()-1] == ']') {
+        if (v.is_atomic() && v.is_string() && v.size() > 1 && v.get_string()[0] == '[') {
             auto pos = p.pos();
             p.next();
             std::string s(v.get_string() + 1);
-            s.pop_back();
+            if (v.get_string()[v.size()-1] == ']')
+                s.pop_back();
             name n(s);
-            if (!is_metaclass(n) && n != get_decls_tk() && n != get_declarations_tk())
+            if (!is_metaclass(n) && n != get_decl_tk() && n != get_declaration_tk())
                 throw parser_error(sstream() << "invalid metaclass name '[" << n << "]'", pos);
+            if (v.get_string()[v.size()-1] != ']') {
+                // Consume ']' for tokens such as `[unfold`
+                p.check_token_next(get_rbracket_tk(), "invalid 'open' command, ']' expected");
+            }
             return optional<name>(n);
         }
     }
@@ -245,12 +252,12 @@ static void parse_metaclasses(parser & p, buffer<name> & r) {
         p.next();
         buffer<name> tmp;
         get_metaclasses(tmp);
-        tmp.push_back(get_decls_tk());
+        tmp.push_back(get_decl_tk());
         while (true) {
             if (optional<name> m = parse_metaclass(p)) {
                 tmp.erase_elem(*m);
-                if (*m == get_declarations_tk())
-                    tmp.erase_elem(get_decls_tk());
+                if (*m == get_declaration_tk())
+                    tmp.erase_elem(get_decl_tk());
             } else {
                 break;
             }
@@ -299,8 +306,8 @@ environment open_export_cmd(parser & p, bool open) {
         parse_metaclasses(p, metacls);
         bool decls = false;
         if (metacls.empty() ||
-            std::find(metacls.begin(), metacls.end(), get_decls_tk()) != metacls.end() ||
-            std::find(metacls.begin(), metacls.end(), get_declarations_tk()) != metacls.end())
+            std::find(metacls.begin(), metacls.end(), get_decl_tk()) != metacls.end() ||
+            std::find(metacls.begin(), metacls.end(), get_declaration_tk()) != metacls.end())
             decls = true;
         for (name const & n : metacls)
             fingerprint = hash(fingerprint, n.hash());
diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp
index 0fad9162c..6930c1ffb 100644
--- a/src/frontends/lean/parser_config.cpp
+++ b/src/frontends/lean/parser_config.cpp
@@ -437,11 +437,11 @@ cmd_table const & get_cmd_table(environment const & env) {
 }
 
 void initialize_parser_config() {
-    token_config::g_class_name = new name("notations");
-    token_config::g_key        = new std::string("tk");
+    token_config::g_class_name = new name("notation");
+    token_config::g_key        = new std::string("TK");
     token_ext::initialize();
-    notation_config::g_class_name = new name("notations");
-    notation_config::g_key        = new std::string("nota");
+    notation_config::g_class_name = new name("notation");
+    notation_config::g_key        = new std::string("NOTA");
     notation_ext::initialize();
     g_ext = new cmd_ext_reg();
 }
diff --git a/src/frontends/lean/tactic_hint.cpp b/src/frontends/lean/tactic_hint.cpp
index de4321559..2c5f5009e 100644
--- a/src/frontends/lean/tactic_hint.cpp
+++ b/src/frontends/lean/tactic_hint.cpp
@@ -57,8 +57,8 @@ template class scoped_ext<tactic_hint_config>;
 typedef scoped_ext<tactic_hint_config> tactic_hint_ext;
 
 void initialize_tactic_hint() {
-    g_class_name = new name("tactic_hints");
-    g_key        = new std::string("tachint");
+    g_class_name = new name("tactic");
+    g_key        = new std::string("TACHINT");
     tactic_hint_ext::initialize();
 }
 
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index a705ccffe..b6ae85cc3 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -63,8 +63,8 @@ static name const * g_instances_tk = nullptr;
 static name const * g_classes_tk = nullptr;
 static name const * g_coercions_tk = nullptr;
 static name const * g_arrow_tk = nullptr;
-static name const * g_declarations_tk = nullptr;
-static name const * g_decls_tk = nullptr;
+static name const * g_declaration_tk = nullptr;
+static name const * g_decl_tk = nullptr;
 static name const * g_hiding_tk = nullptr;
 static name const * g_exposing_tk = nullptr;
 static name const * g_renaming_tk = nullptr;
@@ -213,8 +213,8 @@ void initialize_tokens() {
     g_classes_tk = new name{"classes"};
     g_coercions_tk = new name{"coercions"};
     g_arrow_tk = new name{"->"};
-    g_declarations_tk = new name{"declarations"};
-    g_decls_tk = new name{"decls"};
+    g_declaration_tk = new name{"declaration"};
+    g_decl_tk = new name{"decl"};
     g_hiding_tk = new name{"hiding"};
     g_exposing_tk = new name{"exposing"};
     g_renaming_tk = new name{"renaming"};
@@ -364,8 +364,8 @@ void finalize_tokens() {
     delete g_classes_tk;
     delete g_coercions_tk;
     delete g_arrow_tk;
-    delete g_declarations_tk;
-    delete g_decls_tk;
+    delete g_declaration_tk;
+    delete g_decl_tk;
     delete g_hiding_tk;
     delete g_exposing_tk;
     delete g_renaming_tk;
@@ -514,8 +514,8 @@ name const & get_instances_tk() { return *g_instances_tk; }
 name const & get_classes_tk() { return *g_classes_tk; }
 name const & get_coercions_tk() { return *g_coercions_tk; }
 name const & get_arrow_tk() { return *g_arrow_tk; }
-name const & get_declarations_tk() { return *g_declarations_tk; }
-name const & get_decls_tk() { return *g_decls_tk; }
+name const & get_declaration_tk() { return *g_declaration_tk; }
+name const & get_decl_tk() { return *g_decl_tk; }
 name const & get_hiding_tk() { return *g_hiding_tk; }
 name const & get_exposing_tk() { return *g_exposing_tk; }
 name const & get_renaming_tk() { return *g_renaming_tk; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index cbe0e5e6f..fbcafd71e 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -65,8 +65,8 @@ name const & get_instances_tk();
 name const & get_classes_tk();
 name const & get_coercions_tk();
 name const & get_arrow_tk();
-name const & get_declarations_tk();
-name const & get_decls_tk();
+name const & get_declaration_tk();
+name const & get_decl_tk();
 name const & get_hiding_tk();
 name const & get_exposing_tk();
 name const & get_renaming_tk();
diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt
index 2084e8a40..0981ec4db 100644
--- a/src/frontends/lean/tokens.txt
+++ b/src/frontends/lean/tokens.txt
@@ -58,8 +58,8 @@ instances    instances
 classes      classes
 coercions    coercions
 arrow        ->
-declarations declarations
-decls        decls
+declaration  declaration
+decl         decl
 hiding       hiding
 exposing     exposing
 renaming     renaming
diff --git a/src/library/abbreviation.cpp b/src/library/abbreviation.cpp
index c28ece7d3..5a778612a 100644
--- a/src/library/abbreviation.cpp
+++ b/src/library/abbreviation.cpp
@@ -119,8 +119,8 @@ expr expand_abbreviations(environment const & env, expr const & e) {
 }
 
 void initialize_abbreviation() {
-    g_class_name = new name("abbreviations");
-    g_key        = new std::string("abbrev");
+    g_class_name = new name("abbreviation");
+    g_key        = new std::string("ABBREV");
     abbrev_ext::initialize();
 }
 
diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp
index 0c449e47f..2bc82cbd9 100644
--- a/src/library/aliases.cpp
+++ b/src/library/aliases.cpp
@@ -264,7 +264,7 @@ void open_aliases(lua_State * L) {
 }
 
 void initialize_aliases() {
-    g_aliases = new name("aliases");
+    g_aliases = new name("alias");
     g_ext     = new aliases_ext_reg();
 }
 
diff --git a/src/library/blast/backward/backward_rule_set.cpp b/src/library/blast/backward/backward_rule_set.cpp
index c0dca3c7d..c18a378eb 100644
--- a/src/library/blast/backward/backward_rule_set.cpp
+++ b/src/library/blast/backward/backward_rule_set.cpp
@@ -148,8 +148,8 @@ list<gexpr> backward_rule_set::find(head_index const & h) const {
 }
 
 void initialize_backward_rule_set() {
-    g_class_name = new name("brs");
-    g_key        = new std::string("brs");
+    g_class_name = new name("backward");
+    g_key        = new std::string("BWD");
     brs_ext::initialize();
     register_prio_attribute("intro", "backward chaining",
                             [](environment const & env, io_state const &, name const & d, unsigned prio, name const & ns, bool persistent) {
diff --git a/src/library/blast/grinder/intro_elim_lemmas.cpp b/src/library/blast/grinder/intro_elim_lemmas.cpp
index 32625e4d1..7dc9ec406 100644
--- a/src/library/blast/grinder/intro_elim_lemmas.cpp
+++ b/src/library/blast/grinder/intro_elim_lemmas.cpp
@@ -114,7 +114,7 @@ void get_intro_lemmas(environment const & env, buffer<name> & r) {
 
 void initialize_intro_elim_lemmas() {
     g_class_name = new name("grinder");
-    g_key        = new std::string("grinder");
+    g_key        = new std::string("GRD");
     intro_elim_ext::initialize();
 
     register_prio_attribute("elim", "elimination rule that is eagerly applied by blast grinder",
diff --git a/src/library/blast/simplifier/simp_rule_set.cpp b/src/library/blast/simplifier/simp_rule_set.cpp
index 913f8bbe9..3bb181cfc 100644
--- a/src/library/blast/simplifier/simp_rule_set.cpp
+++ b/src/library/blast/simplifier/simp_rule_set.cpp
@@ -579,8 +579,8 @@ io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets c
 
 void initialize_simplifier_rule_set() {
     g_prefix     = new name(name::mk_internal_unique_name());
-    g_class_name = new name("simps");
-    g_key        = new std::string("simp");
+    g_class_name = new name("simp");
+    g_key        = new std::string("SIMP");
     rrs_ext::initialize();
     register_prio_attribute("simp", "simplification rule",
                             [](environment const & env, io_state const &, name const & d, unsigned prio, name const & ns, bool persistent) {
diff --git a/src/library/class.cpp b/src/library/class.cpp
index 64ad13456..4791cf725 100644
--- a/src/library/class.cpp
+++ b/src/library/class.cpp
@@ -483,7 +483,7 @@ list<expr> get_local_instances(type_checker & tc, list<expr> const & ctx, name c
 void initialize_class() {
     g_tmp_prefix = new name(name::mk_internal_unique_name());
     g_source     = new name("_source");
-    g_class_name = new name("classes");
+    g_class_name = new name("class");
     g_key = new std::string("class");
     class_ext::initialize();
 
diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp
index 289b3ae54..242fa9a01 100644
--- a/src/library/coercion.cpp
+++ b/src/library/coercion.cpp
@@ -373,8 +373,8 @@ environment add_coercion(environment const & env, io_state const &, name const &
 void initialize_coercion() {
     g_fun        = new name("_Fun");
     g_sort       = new name("_Sort");
-    g_class_name = new name("coercions");
-    g_key        = new std::string("coerce");
+    g_class_name = new name("coercion");
+    g_key        = new std::string("COERCE");
     coercion_ext::initialize();
     register_attribute("coercion", "coercion",
                        [](environment const & env, io_state const & ios, name const & d, name const & ns, bool persistent) {
diff --git a/src/library/light_lt_manager.cpp b/src/library/light_lt_manager.cpp
index 78fb68a24..77e8a13a2 100644
--- a/src/library/light_lt_manager.cpp
+++ b/src/library/light_lt_manager.cpp
@@ -191,8 +191,8 @@ io_state_stream const & operator<<(io_state_stream const & out, light_rule_set c
 }
 
 void initialize_light_rule_set() {
-    g_class_name = new name("lrs");
-    g_key        = new std::string("lrs");
+    g_class_name = new name("light");
+    g_key        = new std::string("LIGHT");
     lrs_ext::initialize();
     register_param_attribute("light", "hint for simplifier",
                              [](environment const & env, io_state const &, name const & d, unsigned idx, name const & ns, bool persistent) {
diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index 589d74c26..528efa623 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -163,8 +163,8 @@ environment erase_constructor_hint(environment const & env, name const & n, name
 }
 
 void initialize_normalize() {
-    g_unfold_hint_name = new name("unfold_hints");
-    g_key = new std::string("unfoldh");
+    g_unfold_hint_name = new name("unfold");
+    g_key = new std::string("UNFOLDH");
     unfold_hint_ext::initialize();
     register_params_attribute("unfold", "unfold definition when the given positions are constructors",
                               [](environment const & env, io_state const &, name const & d, list<unsigned> const & idxs, name const & ns, bool persistent) {
diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp
index d95afc66d..51883fc28 100644
--- a/src/library/reducible.cpp
+++ b/src/library/reducible.cpp
@@ -66,8 +66,8 @@ typedef scoped_ext<reducible_config> reducible_ext;
 static name * g_tmp_prefix = nullptr;
 
 void initialize_reducible() {
-    g_class_name = new name("reduce_hints");
-    g_key        = new std::string("redu");
+    g_class_name = new name("reducible");
+    g_key        = new std::string("REDU");
     g_tmp_prefix = new name(name::mk_internal_unique_name());
     reducible_ext::initialize();
 
diff --git a/src/library/relation_manager.cpp b/src/library/relation_manager.cpp
index f3551e0bb..edc138aee 100644
--- a/src/library/relation_manager.cpp
+++ b/src/library/relation_manager.cpp
@@ -327,8 +327,8 @@ is_relation_pred mk_is_relation_pred(environment const & env) {
 }
 
 void initialize_relation_manager() {
-    g_rel_name = new name("rel");
-    g_key       = new std::string("rel");
+    g_rel_name = new name("relation");
+    g_key       = new std::string("REL");
     rel_ext::initialize();
     register_attribute("refl", "reflexive relation",
                        [](environment const & env, io_state const &, name const & d, name const & ns, bool persistent) {
diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp
index ebc63e3b9..d326693e6 100644
--- a/src/library/user_recursors.cpp
+++ b/src/library/user_recursors.cpp
@@ -345,7 +345,7 @@ has_recursors_pred::has_recursors_pred(environment const & env):
 
 void initialize_user_recursors() {
     g_class_name = new name("recursor");
-    g_key        = new std::string("urec");
+    g_key        = new std::string("UREC");
     recursor_ext::initialize();
     register_opt_param_attribute("recursor", "user defined recursor",
                                  [](environment const & env, io_state const &, name const & d, optional<unsigned> const & major, name const & ns, bool persistent) {
diff --git a/tests/lean/bad_open.lean b/tests/lean/bad_open.lean
index 254a12fea..e1e77b70b 100644
--- a/tests/lean/bad_open.lean
+++ b/tests/lean/bad_open.lean
@@ -1,3 +1,3 @@
 open "nat"
 
-open [classes] "nat"
+open [class] "nat"
diff --git a/tests/lean/bad_open.lean.expected.out b/tests/lean/bad_open.lean.expected.out
index ef40eec37..5c2533520 100644
--- a/tests/lean/bad_open.lean.expected.out
+++ b/tests/lean/bad_open.lean.expected.out
@@ -1,2 +1,2 @@
 bad_open.lean:1:5: error: invalid 'open/export' command, identifier expected
-bad_open.lean:3:15: error: invalid 'open/export' command, identifier expected
+bad_open.lean:3:13: error: invalid 'open/export' command, identifier expected
diff --git a/tests/lean/extra/bag.lean b/tests/lean/extra/bag.lean
index 2ff063bbd..7ed165ae7 100644
--- a/tests/lean/extra/bag.lean
+++ b/tests/lean/extra/bag.lean
@@ -7,7 +7,7 @@ Finite bags.
 -/
 import data.nat data.list.perm algebra.binary
 open nat quot list subtype binary function eq.ops algebra
-open [declarations] perm
+open [decl] perm
 
 variable {A : Type}
 
diff --git a/tests/lean/open_tst.lean b/tests/lean/open_tst.lean
index fccc82380..a7336a73a 100644
--- a/tests/lean/open_tst.lean
+++ b/tests/lean/open_tst.lean
@@ -11,7 +11,7 @@ section
 end
 
 section
-  open - [classes] nat
+  open - [class] nat
   variable a : nat
   check a + a
   check add a a
@@ -21,7 +21,7 @@ section
 end
 
 section
-  open - [classes] [decls] nat
+  open - [class] [decl] nat
   variable a : nat
   check a + a
   check a + 1
@@ -30,7 +30,7 @@ section
 end
 
 section
-  open [classes] nat
+  open [class] nat
   definition foo3 : inhabited nat :=
   _
 
diff --git a/tests/lean/run/568.lean b/tests/lean/run/568.lean
index b5ea19483..326c186e6 100644
--- a/tests/lean/run/568.lean
+++ b/tests/lean/run/568.lean
@@ -7,9 +7,9 @@ namespace f2
 end f2
 
 namespace f3
-  export [declarations] f1
-  export - [declarations] f2
+  export [declaration] f1
+  export - [declaration] f2
 end f3
 
-export [declarations] f1
-export - [declarations] f2
+export [declaration] f1
+export - [declaration] f2
diff --git a/tests/lean/run/blast_simp_sum.lean b/tests/lean/run/blast_simp_sum.lean
index f124a239f..289e2aa94 100644
--- a/tests/lean/run/blast_simp_sum.lean
+++ b/tests/lean/run/blast_simp_sum.lean
@@ -1,5 +1,5 @@
 import data.nat
-open - [simps] nat
+open - [simp] nat
 
 definition Sum : nat → (nat → nat) → nat :=
 sorry
diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean
index 91d3336d2..187fe022e 100644
--- a/tests/lean/run/class5.lean
+++ b/tests/lean/run/class5.lean
@@ -31,7 +31,7 @@ section
 end
 
 section
-  open [notations] algebra
+  open [notation] algebra
   open nat
   -- check mul_struct nat  << This is an error, we opened only the notation from algebra
   variables a b c : nat
diff --git a/tests/lean/run/e11.lean b/tests/lean/run/e11.lean
index 064a54bf3..ab7bef72e 100644
--- a/tests/lean/run/e11.lean
+++ b/tests/lean/run/e11.lean
@@ -18,10 +18,10 @@ end int
 
 section
   -- Open "only" the notation and declarations from the namespaces nat and int
-  open [notations] nat
-  open [notations] int
-  open [decls] nat
-  open [decls] int
+  open [notation] nat
+  open [notation] int
+  open [decl] nat
+  open [decl] int
 
   variables n m : nat
   variables i j : int
diff --git a/tests/lean/run/e12.lean b/tests/lean/run/e12.lean
index 7f02d5e2f..13da1cca1 100644
--- a/tests/lean/run/e12.lean
+++ b/tests/lean/run/e12.lean
@@ -20,17 +20,17 @@ constants n m : nat.nat
 constants i j : int.int
 
 section
-  open [notations] nat
-  open [notations] int
-  open [decls] nat
-  open [decls] int
+  open [notation] nat
+  open [notation] int
+  open [decl] nat
+  open [decl] int
   check n+m
   check i+j
   --  check i+n -- Error
 end
 
 namespace int
-  open [decls] nat (nat)
+  open [decl] nat (nat)
   -- Here is a possible trick for this kind of configuration
   definition add_ni (a : nat) (b : int) := (of_nat a) + b
   definition add_in (a : int) (b : nat) := a + (of_nat b)
@@ -39,10 +39,10 @@ namespace int
 end int
 
 section
-  open [notations] nat
-  open [notations] int
-  open [declarations] nat
-  open [declarations] int
+  open [notation] nat
+  open [notation] int
+  open [declaration] nat
+  open [declaration] int
   check n+m
   check i+n
   check n+i
diff --git a/tests/lean/run/e8.lean b/tests/lean/run/e8.lean
index 6891d491e..64f6f7a43 100644
--- a/tests/lean/run/e8.lean
+++ b/tests/lean/run/e8.lean
@@ -17,10 +17,10 @@ attribute of_nat [coercion]
 end int
 
 -- Open "only" the notation and declarations from the namespaces nat and int
-open [notations] nat
-open [notations] int
-open [decls] nat
-open [decls] int
+open [notation] nat
+open [notation] int
+open [decl] nat
+open [decl] int
 
 constants n m : nat
 constants i j : int
diff --git a/tests/lean/run/ppbeta.lean b/tests/lean/run/ppbeta.lean
index cfb78da8d..f1ee15189 100644
--- a/tests/lean/run/ppbeta.lean
+++ b/tests/lean/run/ppbeta.lean
@@ -1,6 +1,6 @@
 import data.int
-open [coercions] [classes] int
-open [coercions] nat
+open [coercion] [class] int
+open [coercion] nat
 
 definition lt1 (a b : int) := int.le (int.add a 1) b
 infix `<`     := lt1
diff --git a/tests/lean/t14.lean b/tests/lean/t14.lean
index 145482b3d..1a22d8132 100644
--- a/tests/lean/t14.lean
+++ b/tests/lean/t14.lean
@@ -41,13 +41,13 @@ section
 end
 
 section
-  open [notations] foo -- use only the notation
+  open [notation] foo -- use only the notation
   check foo.a * foo.c
   check a * c -- Error
 end
 
 section
-  open [decls] foo -- use only the declarations
+  open [decl] foo -- use only the declarations
   check f a c
   check a*c -- Error
 end