diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean
index 20ffa0a86..3ee13e4c1 100644
--- a/hott/algebra/category/adjoint.hlean
+++ b/hott/algebra/category/adjoint.hlean
@@ -35,7 +35,7 @@ namespace category
   abbreviation inverse := @is_equivalence.G
   postfix ⁻¹ := inverse
   --a second notation for the inverse, which is not overloaded
-  postfix [parsing-only] `⁻¹F`:std.prec.max_plus := inverse
+  postfix [parsing_only] `⁻¹F`:std.prec.max_plus := inverse
 
   --TODO: review and change
   definition faithful [class] (F : C ⇒ D) := Π⦃c c' : C⦄ ⦃f f' : c ⟶ c'⦄, F f = F f' → f = f'
diff --git a/hott/algebra/category/category.hlean b/hott/algebra/category/category.hlean
index b58fa4090..40a773212 100644
--- a/hott/algebra/category/category.hlean
+++ b/hott/algebra/category/category.hlean
@@ -18,7 +18,7 @@ namespace category
   structure category [class] (ob : Type) extends parent : precategory ob :=
   mk' :: (iso_of_path_equiv : is_univalent parent)
 
-  attribute category [multiple-instances]
+  attribute category [multiple_instances]
 
   abbreviation iso_of_path_equiv := @category.iso_of_path_equiv
 
diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean
index 247e0fc6d..d04987a00 100644
--- a/hott/algebra/category/iso.hlean
+++ b/hott/algebra/category/iso.hlean
@@ -22,7 +22,7 @@ namespace iso
 
   attribute is_iso.inverse [quasireducible]
 
-  attribute is_iso [multiple-instances]
+  attribute is_iso [multiple_instances]
   open split_mono split_epi is_iso
   abbreviation retraction_of [unfold 6] := @split_mono.retraction_of
   abbreviation retraction_comp [unfold 6] := @split_mono.retraction_comp
@@ -33,7 +33,7 @@ namespace iso
   abbreviation right_inverse [unfold 6] := @is_iso.right_inverse
   postfix ⁻¹ := inverse
   --a second notation for the inverse, which is not overloaded
-  postfix [parsing-only] `⁻¹ʰ`:std.prec.max_plus := inverse -- input using \-1h
+  postfix [parsing_only] `⁻¹ʰ`:std.prec.max_plus := inverse -- input using \-1h
 
   variables {ob : Type} [C : precategory ob]
   variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
@@ -163,7 +163,7 @@ namespace iso
   mk (to_hom H2 ∘ to_hom H1)
 
   infixl ` ⬝i `:75 := iso.trans
-  postfix [parsing-only] `⁻¹ⁱ`:(max + 1) := iso.symm
+  postfix [parsing_only] `⁻¹ⁱ`:(max + 1) := iso.symm
 
   definition iso_mk_eq {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f')
       : iso.mk f = iso.mk f' :=
diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean
index 490b7a8ed..4ad5a356e 100644
--- a/hott/algebra/category/precategory.hlean
+++ b/hott/algebra/category/precategory.hlean
@@ -30,12 +30,12 @@ namespace category
     (id_id : Π (a : ob), comp !ID !ID = ID a)
     (is_hset_hom : Π(a b : ob), is_hset (hom a b))
 
-  attribute precategory [multiple-instances]
+  attribute precategory [multiple_instances]
   attribute precategory.is_hset_hom [instance]
 
   infixr ∘ := precategory.comp
   -- input ⟶ using \--> (this is a different arrow than \-> (→))
-  infixl [parsing-only] ` ⟶ `:25 := precategory.hom
+  infixl [parsing_only] ` ⟶ `:25 := precategory.hom
   namespace hom
     infixl ` ⟶ `:25 := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b
   end hom
diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean
index c6cb4a665..6801e8279 100644
--- a/hott/algebra/group.hlean
+++ b/hott/algebra/group.hlean
@@ -42,7 +42,7 @@ notation 1 := !has_one.one
 notation 0 := !has_zero.zero
 
 --a second notation for the inverse, which is not overloaded
-postfix [parsing-only] `⁻¹ᵍ`:std.prec.max_plus := has_inv.inv
+postfix [parsing_only] `⁻¹ᵍ`:std.prec.max_plus := has_inv.inv
 
 /- semigroup -/
 
diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean
index 89ee1fa4f..cdcf59c45 100644
--- a/hott/init/datatypes.hlean
+++ b/hott/init/datatypes.hlean
@@ -7,8 +7,8 @@ Basic datatypes
 -/
 
 prelude
-notation [parsing-only] `Type'` := Type.{_+1}
-notation [parsing-only] `Type₊` := Type.{_+1}
+notation [parsing_only] `Type'` := Type.{_+1}
+notation [parsing_only] `Type₊` := Type.{_+1}
 notation `Type₀` := Type.{0}
 notation `Type₁` := Type.{1}
 notation `Type₂` := Type.{2}
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index b29987fbb..7e95aa285 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -32,7 +32,7 @@ namespace is_equiv
   /- Some instances and closure properties of equivalences -/
   postfix ⁻¹ := inv
   /- a second notation for the inverse, which is not overloaded -/
-  postfix [parsing-only] `⁻¹ᶠ`:std.prec.max_plus := inv
+  postfix [parsing_only] `⁻¹ᶠ`:std.prec.max_plus := inv
 
   section
   variables {A B C : Type} (f : A → B) (g : B → C) {f' : A → B}
@@ -286,11 +286,11 @@ namespace equiv
   equiv.mk (g ∘ f) !is_equiv_compose
 
   infixl `⬝e`:75 := equiv.trans
-  postfix [parsing-only] `⁻¹ᵉ`:(max + 1) := equiv.symm
+  postfix [parsing_only] `⁻¹ᵉ`:(max + 1) := equiv.symm
     -- notation for inverse which is not overloaded
   abbreviation erfl [constructor] := @equiv.refl
 
-  definition to_inv_trans [reducible] [unfold-full] (f : A ≃ B) (g : B ≃ C)
+  definition to_inv_trans [reducible] [unfold_full] (f : A ≃ B) (g : B ≃ C)
     : to_inv (f ⬝e g) = to_fun (g⁻¹ᵉ ⬝e f⁻¹ᵉ) :=
   idp
 
@@ -371,4 +371,5 @@ namespace is_equiv
 
 end is_equiv
 
-export [unfold-hints] equiv [unfold-hints] is_equiv
+export [unfold_hints] equiv
+export [unfold_hints] is_equiv
diff --git a/hott/init/function.hlean b/hott/init/function.hlean
index cb6e9075f..ae4fa49a5 100644
--- a/hott/init/function.hlean
+++ b/hott/init/function.hlean
@@ -15,39 +15,39 @@ namespace function
 
 variables {A B C D E : Type}
 
-definition compose [reducible] [unfold-full] (f : B → C) (g : A → B) : A → C :=
+definition compose [reducible] [unfold_full] (f : B → C) (g : A → B) : A → C :=
 λx, f (g x)
 
-definition compose_right [reducible] [unfold-full] (f : B → B → B) (g : A → B) : B → A → B :=
+definition compose_right [reducible] [unfold_full] (f : B → B → B) (g : A → B) : B → A → B :=
 λ b a, f b (g a)
 
-definition compose_left [reducible] [unfold-full] (f : B → B → B) (g : A → B) : A → B → B :=
+definition compose_left [reducible] [unfold_full] (f : B → B → B) (g : A → B) : A → B → B :=
 λ a b, f (g a) b
 
-definition id [reducible] [unfold-full] (a : A) : A :=
+definition id [reducible] [unfold_full] (a : A) : A :=
 a
 
-definition on_fun [reducible] [unfold-full] (f : B → B → C) (g : A → B) : A → A → C :=
+definition on_fun [reducible] [unfold_full] (f : B → B → C) (g : A → B) : A → A → C :=
 λx y, f (g x) (g y)
 
-definition combine [reducible] [unfold-full] (f : A → B → C) (op : C → D → E) (g : A → B → D)
+definition combine [reducible] [unfold_full] (f : A → B → C) (op : C → D → E) (g : A → B → D)
   : A → B → E :=
 λx y, op (f x y) (g x y)
 
-definition const [reducible] [unfold-full] (B : Type) (a : A) : B → A :=
+definition const [reducible] [unfold_full] (B : Type) (a : A) : B → A :=
 λx, a
 
-definition dcompose [reducible] [unfold-full] {B : A → Type} {C : Π {x : A}, B x → Type}
+definition dcompose [reducible] [unfold_full] {B : A → Type} {C : Π {x : A}, B x → Type}
   (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) :=
 λx, f (g x)
 
-definition flip [reducible] [unfold-full] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
+definition flip [reducible] [unfold_full] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
 λy x, f x y
 
-definition app [reducible] [unfold-full] {B : A → Type} (f : Πx, B x) (x : A) : B x :=
+definition app [reducible] [unfold_full] {B : A → Type} (f : Πx, B x) (x : A) : B x :=
 f x
 
-definition curry [reducible] [unfold-full] : (A × B → C) → A → B → C :=
+definition curry [reducible] [unfold_full] : (A × B → C) → A → B → C :=
 λ f a b, f (a, b)
 
 definition uncurry [reducible] [unfold 5] : (A → B → C) → (A × B → C) :=
@@ -63,4 +63,4 @@ notation f ` -[` op `]- ` g  := combine f op g
 end function
 
 -- copy reducible annotations to top-level
-export [reduce-hints] [unfold-hints] function
+export [reduce_hints] [unfold_hints] function
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 25071735c..879e19e87 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -41,12 +41,12 @@ namespace eq
   infix   ⬝  := concat
   postfix ⁻¹ := inverse
   --a second notation for the inverse, which is not overloaded
-  postfix [parsing-only] `⁻¹ᵖ`:std.prec.max_plus := inverse
+  postfix [parsing_only] `⁻¹ᵖ`:std.prec.max_plus := inverse
 
   /- The 1-dimensional groupoid structure -/
 
   -- The identity path is a right unit.
-  definition con_idp [unfold-full] (p : x = y) : p ⬝ idp = p :=
+  definition con_idp [unfold_full] (p : x = y) : p ⬝ idp = p :=
   idp
 
   -- The identity path is a right unit.
@@ -195,7 +195,7 @@ namespace eq
   definition cast [reducible] [unfold 3] {A B : Type} (p : A = B) (a : A) : B :=
   p ▸ a
 
-  definition cast_def [reducible] [unfold-full] {A B : Type} (p : A = B) (a : A)
+  definition cast_def [reducible] [unfold_full] {A B : Type} (p : A = B) (a : A)
     : cast p a = p ▸ a :=
   idp
 
@@ -205,21 +205,21 @@ namespace eq
   definition ap [unfold 6] ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x = y) : f x = f y :=
   eq.rec_on p idp
 
-  abbreviation ap01 [parsing-only] := ap
+  abbreviation ap01 [parsing_only] := ap
 
   definition homotopy [reducible] (f g : Πx, P x) : Type :=
   Πx : A, f x = g x
 
   infix ~ := homotopy
 
-  protected definition homotopy.refl [refl] [reducible] [unfold-full] (f : Πx, P x) : f ~ f :=
+  protected definition homotopy.refl [refl] [reducible] [unfold_full] (f : Πx, P x) : f ~ f :=
   λ x, idp
 
-  protected definition homotopy.symm [symm] [reducible] [unfold-full] {f g : Πx, P x} (H : f ~ g)
+  protected definition homotopy.symm [symm] [reducible] [unfold_full] {f g : Πx, P x} (H : f ~ g)
     : g ~ f :=
   λ x, (H x)⁻¹
 
-  protected definition homotopy.trans [trans] [reducible] [unfold-full] {f g h : Πx, P x}
+  protected definition homotopy.trans [trans] [reducible] [unfold_full] {f g h : Πx, P x}
     (H1 : f ~ g) (H2 : g ~ h) : f ~ h :=
   λ x, H1 x ⬝ H2 x
 
@@ -560,7 +560,7 @@ namespace eq
   eq.rec_on h idp
 
   infixl ` ◾ `:75 := concat2
-  postfix [parsing-only] `⁻²`:(max+10) := inverse2 --this notation is abusive, should we use it?
+  postfix [parsing_only] `⁻²`:(max+10) := inverse2 --this notation is abusive, should we use it?
 
   /- Whiskering -/
 
@@ -584,11 +584,11 @@ namespace eq
     whisker_right h idp = h :=
   eq.rec_on h (eq.rec_on p idp)
 
-  definition whisker_right_idp_left [unfold-full] (p : x = y) (q : y = z) :
+  definition whisker_right_idp_left [unfold_full] (p : x = y) (q : y = z) :
     whisker_right idp q = idp :> (p ⬝ q = p ⬝ q) :=
   idp
 
-  definition whisker_left_idp_right [unfold-full] (p : x = y) (q : y = z) :
+  definition whisker_left_idp_right [unfold_full] (p : x = y) (q : y = z) :
     whisker_left p idp = idp :> (p ⬝ q = p ⬝ q) :=
   idp
 
@@ -596,11 +596,11 @@ namespace eq
     (idp_con p) ⁻¹ ⬝ whisker_left idp h ⬝ idp_con q = h :=
   eq.rec_on h (eq.rec_on p idp)
 
-  definition con2_idp [unfold-full] {p q : x = y} (h : p = q) :
+  definition con2_idp [unfold_full] {p q : x = y} (h : p = q) :
     h ◾ idp = whisker_right h idp :> (p ⬝ idp = q ⬝ idp) :=
   idp
 
-  definition idp_con2 [unfold-full] {p q : x = y} (h : p = q) :
+  definition idp_con2 [unfold_full] {p q : x = y} (h : p = q) :
     idp ◾ h = whisker_left idp h :> (idp ⬝ p = idp ⬝ q) :=
   idp
 
diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean
index 1459145bc..9bc7fa939 100644
--- a/hott/init/pathover.hlean
+++ b/hott/init/pathover.hlean
@@ -295,6 +295,6 @@ namespace eq
   by induction s; induction s₂; reflexivity
 
   infixl `◾o`:75 := concato2
-  postfix [parsing-only] `⁻²ᵒ`:(max+10) := inverseo2 --this notation is abusive, should we use it?
+  postfix [parsing_only] `⁻²ᵒ`:(max+10) := inverseo2 --this notation is abusive, should we use it?
 
 end eq
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index 4d0734091..05bd6e85d 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -317,7 +317,7 @@ namespace is_trunc
   protected abbreviation hprop.mk := @trunctype.mk -1
   protected abbreviation hset.mk := @trunctype.mk (-1.+1)
 
-  protected abbreviation trunctype.mk' [parsing-only] (n : trunc_index) (A : Type)
+  protected abbreviation trunctype.mk' [parsing_only] (n : trunc_index) (A : Type)
     [H : is_trunc n A] : n-Type :=
   trunctype.mk A H
 
diff --git a/hott/init/types.hlean b/hott/init/types.hlean
index 19aa3880b..04e864e3c 100644
--- a/hott/init/types.hlean
+++ b/hott/init/types.hlean
@@ -85,7 +85,7 @@ namespace prod
   infixr × := prod
 
   namespace ops
-  infixr [parsing-only] * := prod
+  infixr [parsing_only] * := prod
   postfix `.1`:(max+1) := pr1
   postfix `.2`:(max+1) := pr2
   abbreviation pr₁ := @pr1
diff --git a/hott/init/ua.hlean b/hott/init/ua.hlean
index e3f3a4ae1..f0981462c 100644
--- a/hott/init/ua.hlean
+++ b/hott/init/ua.hlean
@@ -21,7 +21,7 @@ section
   definition equiv_of_eq [constructor] (H : A = B) : A ≃ B :=
   equiv.mk _ (is_equiv_cast_of_eq H)
 
-  definition equiv_of_eq_refl [reducible] [unfold-full] (A : Type)
+  definition equiv_of_eq_refl [reducible] [unfold_full] (A : Type)
     : equiv_of_eq (refl A) = equiv.refl :=
   idp
 
diff --git a/hott/types/arrow.hlean b/hott/types/arrow.hlean
index f8b4d5e62..d5d8cfc53 100644
--- a/hott/types/arrow.hlean
+++ b/hott/types/arrow.hlean
@@ -21,7 +21,7 @@ namespace pi
   /- Functorial action -/
   variables (f0 : A' → A) (f1 : B → B')
 
-  definition arrow_functor [unfold-full] : (A → B) → (A' → B') := pi_functor f0 (λa, f1)
+  definition arrow_functor [unfold_full] : (A → B) → (A' → B') := pi_functor f0 (λa, f1)
 
   /- Equivalences -/
 
diff --git a/hott/types/lift.hlean b/hott/types/lift.hlean
index 8d332bc8d..13fdd7a08 100644
--- a/hott/types/lift.hlean
+++ b/hott/types/lift.hlean
@@ -75,7 +75,7 @@ namespace lift
   definition lift_equiv_lift_refl (A : Type) : lift_equiv_lift (erfl : A ≃ A) = erfl :=
   by apply equiv_eq'; intro z; induction z with a; reflexivity
 
-  definition lift_inv_functor [unfold-full] (a : A) : A' :=
+  definition lift_inv_functor [unfold_full] (a : A) : A' :=
   down (g (up a))
 
   definition is_equiv_lift_inv_functor [constructor] [Hf : is_equiv g]
diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean
index 217c02428..03c88419e 100644
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@@ -155,7 +155,7 @@ namespace pi
 
   /- The functoriality of [forall] is slightly subtle: it is contravariant in the domain type and covariant in the codomain, but the codomain is dependent on the domain. -/
 
-  definition pi_functor [unfold-full] : (Π(a:A), B a) → (Π(a':A'), B' a') := λg a', f1 a' (g (f0 a'))
+  definition pi_functor [unfold_full] : (Π(a:A), B a) → (Π(a':A'), B' a') := λg a', f1 a' (g (f0 a'))
 
   definition ap_pi_functor {g g' : Π(a:A), B a} (h : g ~ g')
     : ap (pi_functor f0 f1) (eq_of_homotopy h)
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index 9798bf34e..afd1bd425 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -402,7 +402,7 @@ namespace sigma
 
   definition subtype [reducible] {A : Type} (P : A → Type) [H : Πa, is_hprop (P a)] :=
   Σ(a : A), P a
-  notation [parsing-only] `{` binder `|` r:(scoped:1 P, subtype P) `}` := r
+  notation [parsing_only] `{` binder `|` r:(scoped:1 P, subtype P) `}` := r
 
   /- To prove equality in a subtype, we only need equality of the first component. -/
   definition subtype_eq [H : Πa, is_hprop (B a)] (u v : {a | B a}) : u.1 = v.1 → u = v :=
diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean
index d2176572d..0fd993a68 100644
--- a/library/algebra/category/basic.lean
+++ b/library/algebra/category/basic.lean
@@ -14,7 +14,7 @@ structure category [class] (ob : Type) : Type :=
   (id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f)
   (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f)
 
-attribute category [multiple-instances]
+attribute category [multiple_instances]
 
 namespace category
   variables {ob : Type} [C : category ob]
diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean
index 97ffc91e0..1f3da406a 100644
--- a/library/algebra/category/morphism.lean
+++ b/library/algebra/category/morphism.lean
@@ -18,7 +18,7 @@ namespace morphism
   inductive is_iso        [class] (f : a ⟶ b) : Type
   := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
 
-  attribute is_iso [multiple-instances]
+  attribute is_iso [multiple_instances]
 
   definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a :=
   is_section.rec (λg h, g) H
diff --git a/library/algebra/field.lean b/library/algebra/field.lean
index 1a7e7e355..7f842a2c0 100644
--- a/library/algebra/field.lean
+++ b/library/algebra/field.lean
@@ -330,7 +330,7 @@ section discrete_field
     (suppose x ≠ 0,
       or.inr (by rewrite [-one_mul, -(inv_mul_cancel this), mul.assoc, H, mul_zero]))
 
-  definition discrete_field.to_integral_domain [trans-instance] [reducible] [coercion] :
+  definition discrete_field.to_integral_domain [trans_instance] [reducible] [coercion] :
     integral_domain A :=
   ⦃ integral_domain, s,
     eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero⦄
diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 6dae42483..ce348eaa7 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -314,12 +314,12 @@ section group
       ... = x ∘c b : Py
       ... = a : Px)
 
-  definition group.to_left_cancel_semigroup [trans-instance] [coercion] [reducible] :
+  definition group.to_left_cancel_semigroup [trans_instance] [coercion] [reducible] :
     left_cancel_semigroup A :=
   ⦃ left_cancel_semigroup, s,
     mul_left_cancel := @mul_left_cancel A s ⦄
 
-  definition group.to_right_cancel_semigroup [trans-instance] [coercion] [reducible] :
+  definition group.to_right_cancel_semigroup [trans_instance] [coercion] [reducible] :
     right_cancel_semigroup A :=
   ⦃ right_cancel_semigroup, s,
     mul_right_cancel := @mul_right_cancel A s ⦄
@@ -442,12 +442,12 @@ section add_group
      ... = (c + b) + -b : H
      ... = c : add_neg_cancel_right
 
-  definition add_group.to_left_cancel_semigroup [trans-instance] [coercion] [reducible] :
+  definition add_group.to_left_cancel_semigroup [trans_instance] [coercion] [reducible] :
     add_left_cancel_semigroup A :=
   ⦃ add_left_cancel_semigroup, s,
     add_left_cancel := @add_left_cancel A s ⦄
 
-  definition add_group.to_add_right_cancel_semigroup [trans-instance] [coercion] [reducible] :
+  definition add_group.to_add_right_cancel_semigroup [trans_instance] [coercion] [reducible] :
     add_right_cancel_semigroup A :=
   ⦃ add_right_cancel_semigroup, s,
     add_right_cancel := @add_right_cancel A s ⦄
diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean
index dde566b5c..7303917b6 100644
--- a/library/algebra/group_bigops.lean
+++ b/library/algebra/group_bigops.lean
@@ -167,7 +167,7 @@ end finset
 section add_monoid
   variable [amB : add_monoid B]
   include amB
-  local attribute add_monoid.to_monoid [trans-instance]
+  local attribute add_monoid.to_monoid [trans_instance]
 
   definition Suml (l : list A) (f : A → B) : B := Prodl l f
 
@@ -196,7 +196,7 @@ end add_monoid
 section add_comm_monoid
   variable [acmB : add_comm_monoid B]
   include acmB
-  local attribute add_comm_monoid.to_comm_monoid [trans-instance]
+  local attribute add_comm_monoid.to_comm_monoid [trans_instance]
 
   theorem Suml_add (l : list A) (f g : A → B) : Suml l (λx, f x + g x) = Suml l f + Suml l g :=
     Prodl_mul l f g
@@ -207,7 +207,7 @@ end add_comm_monoid
 namespace finset
   variable [acmB : add_comm_monoid B]
   include acmB
-  local attribute add_comm_monoid.to_comm_monoid [trans-instance]
+  local attribute add_comm_monoid.to_comm_monoid [trans_instance]
 
   definition Sum (s : finset A) (f : A → B) : B := Prod s f
 
diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean
index 11f95f4c5..b115e7b1b 100644
--- a/library/algebra/group_power.lean
+++ b/library/algebra/group_power.lean
@@ -203,7 +203,7 @@ end ordered_ring
 section add_monoid
 variable [s : add_monoid A]
 include s
-local attribute add_monoid.to_monoid [trans-instance]
+local attribute add_monoid.to_monoid [trans_instance]
 open nat
 
 definition nmul : ℕ → A → A := λ n a, a^n
@@ -233,7 +233,7 @@ section add_comm_monoid
 open nat
 variable [s : add_comm_monoid A]
 include s
-local attribute add_comm_monoid.to_comm_monoid [trans-instance]
+local attribute add_comm_monoid.to_comm_monoid [trans_instance]
 
 theorem nmul_add (n : ℕ) (a b : A) : n ⬝ (a + b) = (n ⬝ a) + (n ⬝ b) := mul_pow a b n
 
@@ -242,7 +242,7 @@ end add_comm_monoid
 section add_group
 variable [s : add_group A]
 include s
-local attribute add_group.to_group [trans-instance]
+local attribute add_group.to_group [trans_instance]
 
 section nat
 open nat
diff --git a/library/algebra/group_set_bigops.lean b/library/algebra/group_set_bigops.lean
index 5e233f454..cc5da4260 100644
--- a/library/algebra/group_set_bigops.lean
+++ b/library/algebra/group_set_bigops.lean
@@ -74,7 +74,7 @@ end Prod
 section Sum
   variable [acmB : add_comm_monoid B]
   include acmB
-  local attribute add_comm_monoid.to_comm_monoid [trans-instance]
+  local attribute add_comm_monoid.to_comm_monoid [trans_instance]
 
   noncomputable definition Sum (s : set A) (f : A → B) : B := Prod s f
 
diff --git a/library/algebra/order.lean b/library/algebra/order.lean
index 9afefb949..4caf59b4a 100644
--- a/library/algebra/order.lean
+++ b/library/algebra/order.lean
@@ -108,7 +108,7 @@ section
   private theorem lt_trans (s' : order_pair A) (a b c: A) (lt_ab : a < b) (lt_bc : b < c) : a < c :=
     lt_of_lt_of_le lt_ab (le_of_lt lt_bc)
 
-  definition order_pair.to_strict_order [trans-instance] [coercion] [reducible] : strict_order A :=
+  definition order_pair.to_strict_order [trans_instance] [coercion] [reducible] : strict_order A :=
   ⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄
 
   theorem gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1
@@ -178,7 +178,7 @@ have ne_ac : a ≠ c, from
   show false, from ne_of_lt' lt_bc eq_bc,
 show a < c, from iff.mpr (lt_iff_le_and_ne) (and.intro le_ac ne_ac)
 
-definition strong_order_pair.to_order_pair [trans-instance] [coercion] [reducible]
+definition strong_order_pair.to_order_pair [trans_instance] [coercion] [reducible]
     [s : strong_order_pair A] : order_pair A :=
 ⦃ order_pair, s,
   lt_irrefl := lt_irrefl',
@@ -193,7 +193,7 @@ structure linear_order_pair [class] (A : Type) extends order_pair A, linear_weak
 structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair A,
     linear_weak_order A
 
-definition linear_strong_order_pair.to_linear_order_pair [trans-instance] [coercion] [reducible]
+definition linear_strong_order_pair.to_linear_order_pair [trans_instance] [coercion] [reducible]
     [s : linear_strong_order_pair A] : linear_order_pair A :=
 ⦃ linear_order_pair, s, strong_order_pair.to_order_pair ⦄
 
diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean
index 40a9373c0..1e2122a9e 100644
--- a/library/algebra/ordered_field.lean
+++ b/library/algebra/ordered_field.lean
@@ -381,7 +381,7 @@ section discrete_linear_ordered_field
       (assume H' : ¬ y < x,
         decidable.inl (le.antisymm (le_of_not_gt H') (le_of_not_gt H))))
 
-  definition discrete_linear_ordered_field.to_discrete_field [trans-instance] [reducible] [coercion]
+  definition discrete_linear_ordered_field.to_discrete_field [trans_instance] [reducible] [coercion]
      :  discrete_field A :=
      ⦃ discrete_field, s, has_decidable_eq := dec_eq_of_dec_lt⦄
 
diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
index fa0cc2ff9..170654fce 100644
--- a/library/algebra/ordered_group.lean
+++ b/library/algebra/ordered_group.lean
@@ -210,7 +210,7 @@ theorem ordered_comm_group.lt_of_add_lt_add_left [s : ordered_comm_group A] {a b
 assert H' : -a + (a + b) < -a + (a + c), from ordered_comm_group.add_lt_add_left _ _ H _,
 by rewrite *neg_add_cancel_left at H'; exact H'
 
-definition ordered_comm_group.to_ordered_cancel_comm_monoid [trans-instance] [coercion] [reducible]
+definition ordered_comm_group.to_ordered_cancel_comm_monoid [trans_instance] [coercion] [reducible]
     [s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
 ⦃ ordered_cancel_comm_monoid, s,
   add_left_cancel       := @add.left_cancel A s,
@@ -582,7 +582,7 @@ structure decidable_linear_ordered_comm_group [class] (A : Type)
     (add_lt_add_left : ∀ a b, lt a b → ∀ c, lt (add c a) (add c b))
 
 definition decidable_linear_ordered_comm_group.to_ordered_comm_group
-      [trans-instance] [reducible] [coercion]
+      [trans_instance] [reducible] [coercion]
    (A : Type) [s : decidable_linear_ordered_comm_group A] : ordered_comm_group A :=
 ⦃ ordered_comm_group, s,
   le_of_lt := @le_of_lt A s,
diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean
index c7559b41f..9a234fc0b 100644
--- a/library/algebra/ordered_ring.lean
+++ b/library/algebra/ordered_ring.lean
@@ -235,7 +235,7 @@ begin
   exact (iff.mp !sub_pos_iff_lt H2)
 end
 
-definition ordered_ring.to_ordered_semiring [trans-instance] [coercion] [reducible]
+definition ordered_ring.to_ordered_semiring [trans_instance] [coercion] [reducible]
     [s : ordered_ring A] :
   ordered_semiring A :=
 ⦃ ordered_semiring, s,
@@ -317,7 +317,7 @@ structure linear_ordered_ring [class] (A : Type)
     extends ordered_ring A, linear_strong_order_pair A :=
   (zero_lt_one : lt zero one)
 
-definition linear_ordered_ring.to_linear_ordered_semiring [trans-instance] [coercion] [reducible]
+definition linear_ordered_ring.to_linear_ordered_semiring [trans_instance] [coercion] [reducible]
     [s : linear_ordered_ring A] :
   linear_ordered_semiring A :=
 ⦃ linear_ordered_semiring, s,
@@ -371,7 +371,7 @@ lt.by_cases
         end))
 
 -- Linearity implies no zero divisors. Doesn't need commutativity.
-definition linear_ordered_comm_ring.to_integral_domain [trans-instance] [coercion] [reducible]
+definition linear_ordered_comm_ring.to_integral_domain [trans_instance] [coercion] [reducible]
     [s: linear_ordered_comm_ring A] : integral_domain A :=
 ⦃ integral_domain, s,
   eq_zero_or_eq_zero_of_mul_eq_zero :=
diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index 8181ebdfe..a965e8843 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -171,7 +171,7 @@ have 0 * a + 0 = 0 * a + 0 * a, from calc
         ... = 0 * a + 0 * a : by rewrite {_*a}ring.right_distrib,
 show 0 * a = 0, from  (add.left_cancel this)⁻¹
 
-definition ring.to_semiring [trans-instance] [coercion] [reducible] [s : ring A] : semiring A :=
+definition ring.to_semiring [trans_instance] [coercion] [reducible] [s : ring A] : semiring A :=
 ⦃ semiring, s,
   mul_zero := ring.mul_zero,
   zero_mul := ring.zero_mul ⦄
@@ -256,7 +256,7 @@ end
 
 structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A
 
-definition comm_ring.to_comm_semiring [trans-instance] [coercion] [reducible] [s : comm_ring A] : comm_semiring A :=
+definition comm_ring.to_comm_semiring [trans_instance] [coercion] [reducible] [s : comm_ring A] : comm_semiring A :=
 ⦃ comm_semiring, s,
   mul_zero := mul_zero,
   zero_mul := zero_mul ⦄
diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index 68ee9ff96..7b0e4c07b 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -8,7 +8,7 @@ Definitions and properties of div and mod, following the SSReflect library.
 Following SSReflect and the SMTlib standard, we define a mod b so that 0 ≤ a mod b < |b| when b ≠ 0.
 -/
 import data.int.order data.nat.div
-open [coercions] [reduce-hints] nat
+open [coercions] [reduce_hints] nat
 open [declarations] [classes] nat (succ)
 open - [notations] algebra
 open eq.ops
diff --git a/library/data/real/division.lean b/library/data/real/division.lean
index ec1b9820e..638f79669 100644
--- a/library/data/real/division.lean
+++ b/library/data/real/division.lean
@@ -642,7 +642,7 @@ section migrate_algebra
     decidable_lt := dec_lt
    ⦄
 
-  local attribute real.discrete_linear_ordered_field [trans-instance]
+  local attribute real.discrete_linear_ordered_field [trans_instance]
   local attribute real.comm_ring [instance]
   local attribute real.ordered_ring [instance]
 
diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean
index 58cc893bb..0993236fb 100644
--- a/library/init/datatypes.lean
+++ b/library/init/datatypes.lean
@@ -7,8 +7,8 @@ Basic datatypes
 -/
 prelude
 notation `Prop`  := Type.{0}
-notation [parsing-only] `Type'` := Type.{_+1}
-notation [parsing-only] `Type₊` := Type.{_+1}
+notation [parsing_only] `Type'` := Type.{_+1}
+notation [parsing_only] `Type₊` := Type.{_+1}
 notation `Type₁` := Type.{1}
 notation `Type₂` := Type.{2}
 notation `Type₃` := Type.{3}
diff --git a/library/init/function.lean b/library/init/function.lean
index a918662e9..18d8315f9 100644
--- a/library/init/function.lean
+++ b/library/init/function.lean
@@ -12,39 +12,39 @@ namespace function
 
 variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
 
-definition compose [reducible] [unfold-full] (f : B → C) (g : A → B) : A → C :=
+definition compose [reducible] [unfold_full] (f : B → C) (g : A → B) : A → C :=
 λx, f (g x)
 
-definition compose_right [reducible] [unfold-full] (f : B → B → B) (g : A → B) : B → A → B :=
+definition compose_right [reducible] [unfold_full] (f : B → B → B) (g : A → B) : B → A → B :=
 λ b a, f b (g a)
 
-definition compose_left [reducible] [unfold-full] (f : B → B → B) (g : A → B) : A → B → B :=
+definition compose_left [reducible] [unfold_full] (f : B → B → B) (g : A → B) : A → B → B :=
 λ a b, f (g a) b
 
-definition id [reducible] [unfold-full] (a : A) : A :=
+definition id [reducible] [unfold_full] (a : A) : A :=
 a
 
-definition on_fun [reducible] [unfold-full] (f : B → B → C) (g : A → B) : A → A → C :=
+definition on_fun [reducible] [unfold_full] (f : B → B → C) (g : A → B) : A → A → C :=
 λx y, f (g x) (g y)
 
-definition combine [reducible] [unfold-full] (f : A → B → C) (op : C → D → E) (g : A → B → D)
+definition combine [reducible] [unfold_full] (f : A → B → C) (op : C → D → E) (g : A → B → D)
   : A → B → E :=
 λx y, op (f x y) (g x y)
 
-definition const [reducible] [unfold-full] (B : Type) (a : A) : B → A :=
+definition const [reducible] [unfold_full] (B : Type) (a : A) : B → A :=
 λx, a
 
-definition dcompose [reducible] [unfold-full] {B : A → Type} {C : Π {x : A}, B x → Type}
+definition dcompose [reducible] [unfold_full] {B : A → Type} {C : Π {x : A}, B x → Type}
   (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) :=
 λx, f (g x)
 
-definition swap [reducible] [unfold-full] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
+definition swap [reducible] [unfold_full] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
 λy x, f x y
 
 definition app [reducible] {B : A → Type} (f : Πx, B x) (x : A) : B x :=
 f x
 
-definition curry [reducible] [unfold-full] : (A × B → C) → A → B → C :=
+definition curry [reducible] [unfold_full] : (A × B → C) → A → B → C :=
 λ f a b, f (a, b)
 
 definition uncurry [reducible] [unfold 5] : (A → B → C) → (A × B → C) :=
@@ -159,4 +159,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 [reduce_hints] [unfold_hints] function
diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index 1f5f6cfa2..d9902b2a6 100644
--- a/library/init/reserved_notation.lean
+++ b/library/init/reserved_notation.lean
@@ -136,13 +136,13 @@ infix ≥    := ge
 infix <    := lt
 infix >    := gt
 
-notation [parsing-only] x ` +[`:65 A:0 `] `:0 y:65   := @add A _ x y
-notation [parsing-only] x ` -[`:65 A:0 `] `:0 y:65   := @sub A _ x y
-notation [parsing-only] x ` *[`:70 A:0 `] `:0 y:70   := @mul A _ x y
-notation [parsing-only] x ` /[`:70 A:0 `] `:0 y:70   := @division A _ x y
-notation [parsing-only] x ` div[`:70 A:0 `] `:0 y:70 := @divide A _ x y
-notation [parsing-only] x ` mod[`:70 A:0 `] `:0 y:70 := @modulo A _ x y
-notation [parsing-only] x ` ≤[`:50 A:0 `] `:0 y:50   := @le A _ x y
-notation [parsing-only] x ` ≥[`:50 A:0 `] `:0 y:50   := @ge A _ x y
-notation [parsing-only] x ` <[`:50 A:0 `] `:0 y:50   := @lt A _ x y
-notation [parsing-only] x ` >[`:50 A:0 `] `:0 y:50   := @gt A _ x y
+notation [parsing_only] x ` +[`:65 A:0 `] `:0 y:65   := @add A _ x y
+notation [parsing_only] x ` -[`:65 A:0 `] `:0 y:65   := @sub A _ x y
+notation [parsing_only] x ` *[`:70 A:0 `] `:0 y:70   := @mul A _ x y
+notation [parsing_only] x ` /[`:70 A:0 `] `:0 y:70   := @division A _ x y
+notation [parsing_only] x ` div[`:70 A:0 `] `:0 y:70 := @divide A _ x y
+notation [parsing_only] x ` mod[`:70 A:0 `] `:0 y:70 := @modulo A _ x y
+notation [parsing_only] x ` ≤[`:50 A:0 `] `:0 y:50   := @le A _ x y
+notation [parsing_only] x ` ≥[`:50 A:0 `] `:0 y:50   := @ge A _ x y
+notation [parsing_only] x ` <[`:50 A:0 `] `:0 y:50   := @lt A _ x y
+notation [parsing_only] x ` >[`:50 A:0 `] `:0 y:50   := @gt A _ x y
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 041714b02..2cfb5b608 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -39,13 +39,13 @@
 (defconst lean-constants-regexp (regexp-opt lean-constants))
 (defconst lean-modifiers
   (--map (s-concat "[" it "]")
-         '("persistent" "notation" "visible" "instance" "trans-instance"
-           "class" "parsing-only" "coercion" "unfold-full" "constructor"
+         '("persistent" "notation" "visible" "instance" "trans_instance"
+           "class" "parsing_only" "coercion" "unfold_full" "constructor"
            "reducible" "irreducible" "semireducible" "quasireducible" "wf"
-           "whnf" "multiple-instances" "none" "decls" "declarations"
+           "whnf" "multiple_instances" "none" "decls" "declarations"
            "coercions" "classes" "symm" "subst" "refl" "trans" "simp" "congr"
-           "notations" "abbreviations" "begin-end-hints" "tactic-hints"
-           "reduce-hints" "unfold-hints" "aliases" "eqv"
+           "notations" "abbreviations" "begin_end_hints" "tactic_hints"
+           "reduce_hints" "unfold_hints" "aliases" "eqv"
            "localrefinfo"))
   "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 972fb9e5a..264371a3a 100644
--- a/src/frontends/lean/begin_end_ext.cpp
+++ b/src/frontends/lean/begin_end_ext.cpp
@@ -78,11 +78,11 @@ 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_class_name = new name("begin_end_hints");
     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");
+    g_begin_end  = new name("begin_end");
+    g_begin_end_element = new name("begin_end_element");
     register_annotation(*g_begin_end);
     register_annotation(*g_begin_end_element);
 }
@@ -98,7 +98,7 @@ void finalize_begin_end_ext() {
 static void check_valid_tactic(environment const & env, expr const & pre_tac) {
     type_checker tc(env);
     if (!tc.is_def_eq(tc.infer(pre_tac).first, get_tactic_type()).first)
-        throw exception("invalid begin-end pre-tactic update, argument is not a tactic");
+        throw exception("invalid begin_end pre-tactic update, argument is not a tactic");
 }
 
 environment add_begin_end_pre_tactic(environment const & env, expr const & pre_tac) {
diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp
index b408488af..68b16af48 100644
--- a/src/frontends/lean/decl_attributes.cpp
+++ b/src/frontends/lean/decl_attributes.cpp
@@ -49,12 +49,12 @@ void decl_attributes::parse(buffer<name> const & ns, parser & p) {
         if (p.curr_is_token(get_instance_tk())) {
             m_is_instance = true;
             if (m_is_trans_instance)
-                throw parser_error("invalid '[instance]' attribute, '[trans-instance]' was already provided", pos);
+                throw parser_error("invalid '[instance]' attribute, '[trans_instance]' was already provided", pos);
             p.next();
         } else if (p.curr_is_token(get_trans_inst_tk())) {
             m_is_trans_instance = true;
             if (m_is_instance)
-                throw parser_error("invalid '[trans-instance]' attribute, '[instance]' was already provided", pos);
+                throw parser_error("invalid '[trans_instance]' attribute, '[instance]' was already provided", pos);
             p.next();
         } else if (p.curr_is_token(get_coercion_tk())) {
             p.next();
@@ -101,8 +101,8 @@ void decl_attributes::parse(buffer<name> const & ns, parser & p) {
             }
         } else if (p.curr_is_token(get_parsing_only_tk())) {
             if (!m_is_abbrev)
-                throw parser_error("invalid '[parsing-only]' attribute, only abbreviations can be "
-                                   "marked as '[parsing-only]'", pos);
+                throw parser_error("invalid '[parsing_only]' attribute, only abbreviations can be "
+                                   "marked as '[parsing_only]'", pos);
             m_is_parsing_only = true;
             p.next();
         } else if (p.curr_is_token(get_unfold_full_tk())) {
diff --git a/src/frontends/lean/tactic_hint.cpp b/src/frontends/lean/tactic_hint.cpp
index f9a6b9379..761f417c8 100644
--- a/src/frontends/lean/tactic_hint.cpp
+++ b/src/frontends/lean/tactic_hint.cpp
@@ -57,7 +57,7 @@ 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_class_name = new name("tactic_hints");
     g_key        = new std::string("tachint");
     tactic_hint_ext::initialize();
 }
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index c06e2788b..d1f1fff11 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -106,17 +106,16 @@ void init_token_table(token_table & t) {
     char const * commands[] =
         {"theorem", "axiom", "axioms", "variable", "protected", "private", "reveal",
          "definition", "example", "coercion", "abbreviation", "noncomputable",
-         "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", "[trans-instance]",
+         "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", "[trans_instance]",
          "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
-         "[simp]", "[congr]", "[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor",
-         "evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold-full]", "[unfold-hints]",
+         "[simp]", "[congr]", "[parsing_only]", "[multiple_instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor",
+         "evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold_full]", "[unfold_hints]",
          "[constructor]", "[unfold", "print",
          "end", "namespace", "section", "prelude", "help",
          "import", "inductive", "record", "structure", "module", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
          "tactic_infixl", "tactic_infixr", "tactic_infix", "tactic_postfix", "tactic_prefix", "tactic_notation",
-         "exit", "set_option", "open", "export", "override", "calc_subst", "calc_refl", "calc_trans",
-         "calc_symm", "tactic_hint",
+         "exit", "set_option", "open", "export", "override", "tactic_hint",
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
          "multiple_instances", "find_decl", "attribute", "persistent",
          "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 8a63075e2..57255c605 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -253,19 +253,19 @@ void initialize_tokens() {
     g_variable_tk = new name{"variable"};
     g_variables_tk = new name{"variables"};
     g_instance_tk = new name{"[instance]"};
-    g_trans_inst_tk = new name{"[trans-instance]"};
+    g_trans_inst_tk = new name{"[trans_instance]"};
     g_priority_tk = new name{"[priority"};
     g_unfold_tk = new name{"[unfold"};
-    g_unfold_full_tk = new name{"[unfold-full]"};
-    g_unfold_hints_bracket_tk = new name{"[unfold-hints]"};
-    g_unfold_hints_tk = new name{"unfold-hints"};
+    g_unfold_full_tk = new name{"[unfold_full]"};
+    g_unfold_hints_bracket_tk = new name{"[unfold_hints]"};
+    g_unfold_hints_tk = new name{"unfold_hints"};
     g_constructor_tk = new name{"[constructor]"};
     g_coercion_tk = new name{"[coercion]"};
     g_reducible_tk = new name{"[reducible]"};
     g_quasireducible_tk = new name{"[quasireducible]"};
     g_semireducible_tk = new name{"[semireducible]"};
     g_irreducible_tk = new name{"[irreducible]"};
-    g_parsing_only_tk = new name{"[parsing-only]"};
+    g_parsing_only_tk = new name{"[parsing_only]"};
     g_symm_tk = new name{"[symm]"};
     g_trans_tk = new name{"[trans]"};
     g_refl_tk = new name{"[refl]"};
@@ -276,7 +276,7 @@ void initialize_tokens() {
     g_attribute_tk = new name{"attribute"};
     g_with_tk = new name{"with"};
     g_class_tk = new name{"[class]"};
-    g_multiple_instances_tk = new name{"[multiple-instances]"};
+    g_multiple_instances_tk = new name{"[multiple_instances]"};
     g_prev_tk = new name{"prev"};
     g_scoped_tk = new name{"scoped"};
     g_foldr_tk = new name{"foldr"};
diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt
index 67b635c42..1a29e9681 100644
--- a/src/frontends/lean/tokens.txt
+++ b/src/frontends/lean/tokens.txt
@@ -95,19 +95,19 @@ constants    constants
 variable     variable
 variables    variables
 instance     [instance]
-trans_inst   [trans-instance]
+trans_inst   [trans_instance]
 priority     [priority
 unfold       [unfold
-unfold_full  [unfold-full]
-unfold_hints_bracket [unfold-hints]
-unfold_hints unfold-hints
+unfold_full  [unfold_full]
+unfold_hints_bracket [unfold_hints]
+unfold_hints unfold_hints
 constructor  [constructor]
 coercion     [coercion]
 reducible    [reducible]
 quasireducible [quasireducible]
 semireducible [semireducible]
 irreducible  [irreducible]
-parsing_only [parsing-only]
+parsing_only [parsing_only]
 symm         [symm]
 trans        [trans]
 refl         [refl]
@@ -118,7 +118,7 @@ recursor     [recursor
 attribute    attribute
 with         with
 class        [class]
-multiple_instances [multiple-instances]
+multiple_instances [multiple_instances]
 prev         prev
 scoped       scoped
 foldr        foldr
diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index 3c070ba42..cac62e97b 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -134,7 +134,7 @@ environment erase_unfold_hint(environment const & env, name const & n, bool pers
 environment add_unfold_full_hint(environment const & env, name const & n, bool persistent) {
     declaration const & d = env.get(n);
     if (!d.is_definition())
-        throw exception("invalid [unfold-full] hint, declaration must be a non-opaque definition");
+        throw exception("invalid [unfold_full] hint, declaration must be a non-opaque definition");
     return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_full_entry(n), persistent);
 }
 
@@ -162,7 +162,7 @@ environment erase_constructor_hint(environment const & env, name const & n, bool
 }
 
 void initialize_normalize() {
-    g_unfold_hint_name = new name("unfold-hints");
+    g_unfold_hint_name = new name("unfold_hints");
     g_key = new std::string("unfoldh");
     unfold_hint_ext::initialize();
 }
diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp
index 59fe3f6b9..5e977b39f 100644
--- a/src/library/reducible.cpp
+++ b/src/library/reducible.cpp
@@ -65,7 +65,7 @@ typedef scoped_ext<reducible_config> reducible_ext;
 static name * g_tmp_prefix = nullptr;
 
 void initialize_reducible() {
-    g_class_name = new name("reduce-hints");
+    g_class_name = new name("reduce_hints");
     g_key        = new std::string("redu");
     g_tmp_prefix = new name(name::mk_internal_unique_name());
     reducible_ext::initialize();
diff --git a/src/vim/syntax/lean.vim b/src/vim/syntax/lean.vim
index ba49d29a4..c9b4f958c 100644
--- a/src/vim/syntax/lean.vim
+++ b/src/vim/syntax/lean.vim
@@ -5,7 +5,7 @@
 " For version 5.x: Clear all syntax items
 " For version 6.x: Quit when a syntax file was already loaded
 if version < 600
-	syntax clear
+        syntax clear
 "elseif exists("b:current_syntax")
 "	finish
 endif
@@ -44,11 +44,11 @@ syn keyword leanConstant ≠ < > ≤ ≥ ¬ <= >= ⁻¹ ⬝ ▸ + * - / λ
 syn keyword leanConstant → ∃ ∀
 
 " modifiers (pragmas)
-syn keyword leanModifier contained containedin=leanBracketEncl persistent notation visible instance trans-instance class parsing-only
-syn keyword leanModifier contained containedin=leanBracketEncl coercion unfold-full constructor reducible irreducible semireducible
-syn keyword leanModifier contained containedin=leanBracketEncl quasireducible wf whnf multiple-instances none decls declarations coercions
+syn keyword leanModifier contained containedin=leanBracketEncl persistent notation visible instance trans_instance class parsing_only
+syn keyword leanModifier contained containedin=leanBracketEncl coercion unfold_full constructor reducible irreducible semireducible
+syn keyword leanModifier contained containedin=leanBracketEncl quasireducible wf whnf multiple_instances none decls declarations coercions
 syn keyword leanModifier contained containedin=leanBracketEncl classes symm subst refl trans simp congr notations abbreviations
-syn keyword leanModifier contained containedin=leanBracketEncl begin-end-hints tactic-hints reduce-hints unfold-hints aliases eqv
+syn keyword leanModifier contained containedin=leanBracketEncl begin_end_hints tactic_hints reduce_hints unfold_hints aliases eqv
 syn keyword leanModifier contained containedin=leanBracketEncl localrefinfo
 
 " delimiters