diff --git a/library/standard/hott/path.lean b/library/standard/hott/path.lean
index f9ce679d4..c820c6dd2 100644
--- a/library/standard/hott/path.lean
+++ b/library/standard/hott/path.lean
@@ -466,14 +466,14 @@ induction_on p idp
 -- Transporting in particular fibrations
 -- -------------------------------------
 
-(-- From the Coq HoTT library:
+/-
+From the Coq HoTT library:
 
 One frequently needs lemmas showing that transport in a certain dependent type is equal to some
 more explicitly defined operation, defined according to the structure of that dependent type.
 For most dependent types, we prove these lemmas in the appropriate file in the types/
 subdirectory.  Here we consider only the most basic cases.
-
---)
+-/
 
 -- Transporting in a constant fibration.
 definition transport_const {A B : Type} {x1 x2 : A} (p : x1 ≈ x2) (y : B) :
@@ -640,7 +640,7 @@ definition apD02_pp {A} (B : A → Type) (f : Π x:A, B x) {x y : A}
 induction_on r1 (take r2, induction_on r2 (induction_on p1 idp)) r2
 
 
-(-- From the Coq version:
+/- From the Coq version:
 
 -- ** Tactics, hints, and aliases
 
@@ -691,4 +691,4 @@ Hint Rewrite
 Ltac hott_simpl :=
   autorewrite with paths in * |- * ; auto with path_hints.
 
---)
\ No newline at end of file
+-/
\ No newline at end of file
diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp
index 610c1e601..da7f422ae 100644
--- a/src/frontends/lean/scanner.cpp
+++ b/src/frontends/lean/scanner.cpp
@@ -228,8 +228,8 @@ bool scanner::consume(char const * str, char const * error_msg) {
     }
 }
 
-static char const * g_begin_comment_block = "(--";
-static char const * g_end_comment_block = "--)";
+static char const * g_begin_comment_block = "/-";
+static char const * g_end_comment_block = "-/";
 
 void scanner::read_comment_block() {
     static char const * end_error_msg = "unexpected end of comment block";
@@ -422,7 +422,7 @@ auto scanner::read_key_cmd_id() -> token_kind {
 
 static name g_begin_script_tk("(*");
 static name g_begin_comment_tk("--");
-static name g_begin_comment_block_tk("(--");
+static name g_begin_comment_block_tk("/-");
 
 auto scanner::scan(environment const & env) -> token_kind {
     m_tokens = &get_token_table(env);
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index f93c95910..f8d1c6705 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -70,7 +70,7 @@ token_table init_token_table() {
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type'", g_max_prec},
          {"|", 0}, {"!", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
-         {"(*", 0}, {"(--", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec},
+         {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec},
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 
     char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion",
diff --git a/src/tests/frontends/lean/scanner.cpp b/src/tests/frontends/lean/scanner.cpp
index df373a4c3..f6f675ea9 100644
--- a/src/tests/frontends/lean/scanner.cpp
+++ b/src/tests/frontends/lean/scanner.cpp
@@ -143,8 +143,8 @@ static void tst2() {
     env = add_token(env, "+", 0);
     check("x+y", {tk::Identifier, tk::Keyword, tk::Identifier}, env);
     check("-- testing", {});
-    check("(-- testing --)", {});
-    check("(-- (-- testing\n --) --)", {});
+    check("/- testing -/", {});
+    check("/- /- testing\n -/ -/", {});
     check(" 2.31  ", {tk::Decimal});
     check("2.31", {tk::Decimal});
     check(" 333 22", {tk::Numeral, tk::Numeral});
diff --git a/tests/lean/slow/path_groupoids.lean b/tests/lean/slow/path_groupoids.lean
index 8eaedfcc7..6aa5e7eb5 100644
--- a/tests/lean/slow/path_groupoids.lean
+++ b/tests/lean/slow/path_groupoids.lean
@@ -460,14 +460,14 @@ induction_on p idp
 -- Transporting in particular fibrations
 -- -------------------------------------
 
-(-- From the Coq HoTT library:
+/-
+From the Coq HoTT library:
 
 One frequently needs lemmas showing that transport in a certain dependent type is equal to some
 more explicitly defined operation, defined according to the structure of that dependent type.
 For most dependent types, we prove these lemmas in the appropriate file in the types/
 subdirectory.  Here we consider only the most basic cases.
-
---)
+-/
 
 -- Transporting in a constant fibration.
 definition transport_const {A B : Type} {x1 x2 : A} (p : x1 ≈ x2) (y : B) :