diff --git a/tests/lean/run/e11.lean b/tests/lean/run/e11.lean
index f04676ed7..e44e353d9 100644
--- a/tests/lean/run/e11.lean
+++ b/tests/lean/run/e11.lean
@@ -18,8 +18,8 @@ end int
 
 section
   -- Open "only" the notation and declarations from the namespaces nat and int
-  open [notation] nat
-  open [notation] int
+  open [notations] nat
+  open [notations] int
   open [decls] nat
   open [decls] int
 
diff --git a/tests/lean/run/e12.lean b/tests/lean/run/e12.lean
index dc6482ddb..c71f8dce7 100644
--- a/tests/lean/run/e12.lean
+++ b/tests/lean/run/e12.lean
@@ -20,8 +20,8 @@ constants n m : nat.nat
 constants i j : int.int
 
 section
-  open [notation] nat
-  open [notation] int
+  open [notations] nat
+  open [notations] int
   open [decls] nat
   open [decls] int
   check n+m
@@ -39,8 +39,8 @@ namespace int
 end int
 
 section
-  open [notation] nat
-  open [notation] int
+  open [notations] nat
+  open [notations] int
   open [declarations] nat
   open [declarations] int
   check n+m
diff --git a/tests/lean/run/e8.lean b/tests/lean/run/e8.lean
index ff2096575..28ac4fcd0 100644
--- a/tests/lean/run/e8.lean
+++ b/tests/lean/run/e8.lean
@@ -17,8 +17,8 @@ namespace int
 end int
 
 -- Open "only" the notation and declarations from the namespaces nat and int
-open [notation] nat
-open [notation] int
+open [notations] nat
+open [notations] int
 open [decls] nat
 open [decls] int
 
diff --git a/tests/lean/t14.lean b/tests/lean/t14.lean
index 13e3b6391..fc566b95f 100644
--- a/tests/lean/t14.lean
+++ b/tests/lean/t14.lean
@@ -41,7 +41,7 @@ context
 end
 
 context
-  open [notation] foo -- use only the notation
+  open [notations] foo -- use only the notation
   check foo.a * foo.c
   check a * c -- Error
 end