diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean
index 83aefb7493..fa143c85d4 100644
--- a/library/init/data/option/basic.lean
+++ b/library/init/data/option/basic.lean
@@ -23,6 +23,10 @@ def is_some {α : Type u} : option α → bool
 | (some _) := tt
 | none     := ff
 
+def is_none {α : Type u} : option α → bool
+| (some _) := ff
+| none     := tt
+
 end option
 
 instance (α : Type u) : inhabited (option α) :=
diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean
index f66831f18e..d0745feac4 100644
--- a/library/init/meta/environment.lean
+++ b/library/init/meta/environment.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.declaration init.meta.exceptional
+import init.meta.declaration init.meta.exceptional init.data.option.basic
 
 meta constant environment : Type
 
@@ -93,6 +93,11 @@ match (refl_for env (const_name (get_app_fn e))) with
     else none
 | none   := none
 end
+
+/-- Return true if 'n' has been declared in the current file -/
+meta def in_current_file (env : environment) (n : name) : bool :=
+(env^.decl_olean n)^.is_none && env^.contains n
+
 end environment
 
 meta instance : has_to_string environment :=
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index c1460a7c40..58ba11fbc3 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -931,6 +931,12 @@ do m ← mk_meta_var type,
    set_goals gs,
    return (a, m)
 
+/-- Return tt iff 'd' is a declaration in one of the current open namespaces -/
+meta def in_open_namespaces (d : name) : tactic bool :=
+do ns  ← open_namespaces,
+   env ← get_env,
+   return $ ns^.any (λ n, n^.is_prefix_of d) && env^.contains d
+
 end tactic
 
 open tactic