diff --git a/tests/lean/interactive/completion2.lean b/tests/lean/interactive/completion2.lean
new file mode 100644
index 0000000000..e00c060b55
--- /dev/null
+++ b/tests/lean/interactive/completion2.lean
@@ -0,0 +1,40 @@
+namespace Foo
+namespace Bla
+
+theorem ex1 {a b : Nat} (h : a ≤ b) : a + a ≤ b + b :=
+  sorry
+
+theorem ex2 {a b : Nat} (h : a ≤ b) : a + 2 ≤ b + 2 :=
+  sorry
+
+theorem ex3 {a b c d : Nat} (h : a ≤ b) (h : c ≤ d) : a + c ≤ b + d :=
+  sorry
+
+theorem ax1 {a b : Nat} (h : a ≤ b) : a - a ≤ b - b :=
+  sorry
+
+end Bla
+end Foo
+
+theorem tst1 (h : a ≤ b) : a + 2 ≤ b + 2 :=
+  Foo.Bla.
+        --^ textDocument/completion
+#print ""
+
+open Foo in
+theorem tst2 (h : a ≤ b) : a + 2 ≤ b + 2 :=
+  Bla.
+    --^ textDocument/completion
+#print ""
+
+theorem tst3 (h : a ≤ b) : a + 2 ≤ b + 2 :=
+  let aux := Foo.Bla.  -- we don't have the expected type here
+                   --^ textDocument/completion
+  aux
+
+#print ""
+
+theorem tst4 (h : a ≤ b) : a + 2 ≤ b + 2 :=
+  let aux := Foo.Bla.e  -- we don't have the expected type here
+                    --^ textDocument/completion
+  aux
diff --git a/tests/lean/interactive/completion2.lean.expected.out b/tests/lean/interactive/completion2.lean.expected.out
new file mode 100644
index 0000000000..685f8458bf
--- /dev/null
+++ b/tests/lean/interactive/completion2.lean.expected.out
@@ -0,0 +1,31 @@
+{"textDocument": {"uri": "file://completion2.lean"},
+ "position": {"line": 19, "character": 10}}
+{"items":
+ [{"label": "ex2", "detail": "?a ≤ ?b → ?a + 2 ≤ ?b + 2"},
+  {"label": "ex3", "detail": "?a ≤ ?b → ?c ≤ ?d → ?a + ?c ≤ ?b + ?d"},
+  {"label": "ax1", "detail": "?a ≤ ?b → ?a - ?a ≤ ?b - ?b"},
+  {"label": "ex1", "detail": "?a ≤ ?b → ?a + ?a ≤ ?b + ?b"}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file://completion2.lean"},
+ "position": {"line": 25, "character": 6}}
+{"items":
+ [{"label": "ex2", "detail": "?a ≤ ?b → ?a + 2 ≤ ?b + 2"},
+  {"label": "ex3", "detail": "?a ≤ ?b → ?c ≤ ?d → ?a + ?c ≤ ?b + ?d"},
+  {"label": "ax1", "detail": "?a ≤ ?b → ?a - ?a ≤ ?b - ?b"},
+  {"label": "ex1", "detail": "?a ≤ ?b → ?a + ?a ≤ ?b + ?b"}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file://completion2.lean"},
+ "position": {"line": 30, "character": 21}}
+{"items":
+ [{"label": "ex1", "detail": "?a ≤ ?b → ?a + ?a ≤ ?b + ?b"},
+  {"label": "ex2", "detail": "?a ≤ ?b → ?a + 2 ≤ ?b + 2"},
+  {"label": "ex3", "detail": "?a ≤ ?b → ?c ≤ ?d → ?a + ?c ≤ ?b + ?d"},
+  {"label": "ax1", "detail": "?a ≤ ?b → ?a - ?a ≤ ?b - ?b"}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file://completion2.lean"},
+ "position": {"line": 35, "character": 22}}
+{"items":
+ [{"label": "ex2", "detail": "?a ≤ ?b → ?a + 2 ≤ ?b + 2"},
+  {"label": "ex3", "detail": "?a ≤ ?b → ?c ≤ ?d → ?a + ?c ≤ ?b + ?d"},
+  {"label": "ex1", "detail": "?a ≤ ?b → ?a + ?a ≤ ?b + ?b"}],
+ "isIncomplete": true}