diff --git a/tests/lean/run/e8.lean b/tests/lean/run/e8.lean
new file mode 100644
index 0000000000..cf7ab93c47
--- /dev/null
+++ b/tests/lean/run/e8.lean
@@ -0,0 +1,39 @@
+precedence `+`:65
+
+namespace nat
+  variable nat : Type.{1}
+  variable add : nat → nat → nat
+  infixl + := add
+end
+
+namespace int
+  using nat (nat)
+  variable int : Type.{1}
+  variable add : int → int → int
+  infixl + := add
+  variable of_nat : nat → int
+  coercion of_nat
+end
+
+-- Using "only" the notation and declarations from the namespaces nat and int
+using [notation] nat
+using [notation] int
+using [decls] nat
+using [decls] int
+
+variables n m : nat
+variables i j : int
+check n + m
+check i + j
+
+-- The following check does not work, since we are not using the coercions
+-- check n + i
+
+-- 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)
+infixl + := add_ni
+infixl + := add_in
+
+check i + n
+check n + i
diff --git a/tests/lean/run/e9.lean b/tests/lean/run/e9.lean
new file mode 100644
index 0000000000..01942c2509
--- /dev/null
+++ b/tests/lean/run/e9.lean
@@ -0,0 +1,38 @@
+precedence `+`:65
+
+namespace nat
+  variable nat : Type.{1}
+  variable add : nat → nat → nat
+  infixl + := add
+end
+
+namespace int
+  using nat (nat)
+  variable int : Type.{1}
+  variable add : int → int → int
+  infixl + := add
+  variable of_nat : nat → int
+end
+
+namespace int_coercions
+  coercion int.of_nat
+end
+
+-- Using "only" the notation and declarations from the namespaces nat and int
+using nat
+using int
+
+variables n m : nat
+variables i j : int
+check n + m
+check i + j
+
+section
+  -- Temporarily use the int_coercions
+  using int_coercions
+  check n + i
+end
+
+-- The following one is an error
+-- check n + i
+