diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean
index d0cd58fd92..63b5afbd01 100644
--- a/library/init/meta/environment.lean
+++ b/library/init/meta/environment.lean
@@ -78,8 +78,8 @@ meta constant trans_for : environment → name → option name
 /- (decl_olean env d) returns the name of the .olean file where d was defined.
    The result is none if d was not defined in an imported file. -/
 meta constant decl_olean : environment → name → option string
-/- (decl_pos_info env d) returns the line and column number where d was defined. -/
-meta constant decl_pos_info : environment → name → option (nat × nat)
+/- (decl_pos env d) returns the source location of d if available. -/
+meta constant decl_pos_info : environment → name → option pos
 open expr
 
 meta constant unfold_untrusted_macros : environment → expr → expr
diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index 8ad2753508..4d42fe1b53 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -6,6 +6,16 @@ Authors: Leonardo de Moura
 prelude
 import init.meta.level
 
+structure pos :=
+(line   : nat)
+(column : nat)
+
+instance : decidable_eq pos
+| ⟨l₁, c₁⟩ ⟨l₂, c₂⟩ := if h₁ : l₁ = l₂ then
+  if h₂ : c₁ = c₂ then is_true (eq.rec_on h₁ (eq.rec_on h₂ rfl))
+  else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₂ h₂))
+else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₁ h₁))
+
 inductive binder_info
 | default | implicit | strict_implicit | inst_implicit | other
 
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 3b6616f596..093b189b92 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -13,7 +13,6 @@ open lean.parser
 
 local postfix ?:9001 := optional
 local postfix *:9001 := many
-local notation p ` ?: `:100 d := (λ o, option.get_or_else o d) <$> p?
 
 namespace interactive
 /-- (parse p) as the parameter type of an interactive tactic will instruct the Lean parser
@@ -31,11 +30,11 @@ meta def list_of (p : parser α) := tk "[" *> sep_by "," p <* tk "]"
     trailing expression parameters. -/
 meta def texpr := qexpr 2
 meta def using_ident := (tk "using" *> ident)?
-meta def with_ident_list := (tk "with" *> ident*) ?: []
-meta def without_ident_list := (tk "without" *> ident*) ?: []
-meta def location := (tk "at" *> ident*) ?: []
+meta def with_ident_list := (tk "with" *> ident*) <|> return []
+meta def without_ident_list := (tk "without" *> ident*) <|> return []
+meta def location := (tk "at" *> ident*) <|> return []
 meta def qexpr_list := list_of (qexpr 0)
-meta def opt_qexpr_list := qexpr_list ?: []
+meta def opt_qexpr_list := qexpr_list <|> return []
 meta def qexpr_list_or_texpr := qexpr_list <|> return <$> texpr
 end types
 end interactive
@@ -206,7 +205,7 @@ match e with
 end
 
 private meta def maybe_save_info : option pos → tactic unit
-| (some p) := save_info p.1 p.2
+| (some p) := save_info p
 | none     := skip
 
 private meta def symm_expr := bool × expr × option pos
diff --git a/library/init/meta/pexpr.lean b/library/init/meta/pexpr.lean
index 35049feea9..28a1ff52ec 100644
--- a/library/init/meta/pexpr.lean
+++ b/library/init/meta/pexpr.lean
@@ -7,8 +7,6 @@ prelude
 import init.meta.expr
 universe u
 
-@[reducible] def pos := nat × nat
-
 /- Quoted expressions. They can be converted into expressions by using a tactic. -/
 meta constant pexpr : Type
 protected meta constant pexpr.of_expr  : expr → pexpr
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index 647cd424fc..65177d0d84 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -8,9 +8,9 @@ import init.meta.smt.smt_tactic init.meta.interactive
 import init.meta.smt.rsimp
 
 namespace smt_tactic
-meta def save_info (line : nat) (col : nat) : smt_tactic unit :=
+meta def save_info (p : pos) : smt_tactic unit :=
 do (ss, ts) ← smt_tactic.read,
-   tactic.save_info_thunk line col (λ _, smt_state.to_format ss ts)
+   tactic.save_info_thunk p (λ _, smt_state.to_format ss ts)
 
 meta def skip : smt_tactic unit :=
 return ()
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 1a22f023b3..28a89cf7a9 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -424,7 +424,7 @@ meta constant decl_name : tactic name
 
 /- (save_type_info e ref) save (typeof e) at position associated with ref -/
 meta constant save_type_info : expr → expr → tactic unit
-meta constant save_info_thunk : nat → nat → (unit → format) → tactic unit
+meta constant save_info_thunk : pos → (unit → format) → tactic unit
 meta constant report_error : nat → nat → format → tactic unit
 /-- Return list of currently open namespaces -/
 meta constant open_namespaces : tactic (list name)
@@ -577,9 +577,9 @@ do { ctx ← local_context,
      exact H }
 <|> fail "assumption tactic failed"
 
-meta def save_info (line : nat) (col : nat) : tactic unit :=
+meta def save_info (p : pos) : tactic unit :=
 do s ← read,
-   tactic.save_info_thunk line col (λ _, tactic_state.to_format s)
+   tactic.save_info_thunk p (λ _, tactic_state.to_format s)
 
 notation `‹` p `›` := show p, by assumption
 
diff --git a/library/init/meta/vm.lean b/library/init/meta/vm.lean
index e752435a83..02f428b591 100644
--- a/library/init/meta/vm.lean
+++ b/library/init/meta/vm.lean
@@ -59,8 +59,8 @@ meta constant to_name   : vm_decl → name
 meta constant idx       : vm_decl → nat
 /- Number of arguments needed to execute the given VM declaration. -/
 meta constant arity     : vm_decl → nat
-/- Return (line, column) if available -/
-meta constant pos       : vm_decl → option (nat × nat)
+/- Return source position if available -/
+meta constant pos       : vm_decl → option pos
 /- Return .olean file where the given VM declaration was imported from. -/
 meta constant olean     : vm_decl → option string
 /- Return names .olean file where the given VM declaration was imported from. -/
diff --git a/library/tools/debugger/util.lean b/library/tools/debugger/util.lean
index 3188032781..96020ad1ae 100644
--- a/library/tools/debugger/util.lean
+++ b/library/tools/debugger/util.lean
@@ -44,10 +44,10 @@ return "[current file]"
 
 meta def pos_info (fn : name) : vm string :=
 do {
-  d                ← vm.get_decl fn,
-  some (line, col) ← return (vm_decl.pos d) | failure,
-  file             ← get_file fn,
-  return (file ++ ":" ++ line^.to_string ++ ":" ++ col^.to_string)
+  d      ← vm.get_decl fn,
+  some p ← return (vm_decl.pos d) | failure,
+  file   ← get_file fn,
+  return (file ++ ":" ++ p^.line^.to_string ++ ":" ++ p^.column^.to_string)
 }
 <|>
 return "<position not available>"
diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp
index 430fef4ba8..af0ef15e5c 100644
--- a/src/frontends/lean/info_manager.cpp
+++ b/src/frontends/lean/info_manager.cpp
@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_nat.h"
 #include "library/vm/vm_format.h"
 #include "library/vm/vm_list.h"
+#include "library/vm/vm_pos_info.h"
 #include "library/tactic/tactic_state.h"
 #include "frontends/lean/json.h"
 #include "frontends/lean/info_manager.h"
@@ -151,10 +152,11 @@ info_manager * get_global_info_manager() {
     return g_info_m;
 }
 
-vm_obj tactic_save_info_thunk(vm_obj const & line, vm_obj const & col, vm_obj const & thunk, vm_obj const & s) {
+vm_obj tactic_save_info_thunk(vm_obj const & pos, vm_obj const & thunk, vm_obj const & s) {
     try {
         if (g_info_m) {
-            g_info_m->add_vm_obj_format_info(force_to_unsigned(line), force_to_unsigned(col), tactic::to_state(s).env(), thunk);
+            auto _pos = to_pos_info(pos);
+            g_info_m->add_vm_obj_format_info(_pos.first, _pos.second, tactic::to_state(s).env(), thunk);
         }
         return tactic::mk_success(tactic::to_state(s));
     } catch (exception & ex) {
diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index 719a053d36..c1f3a2aeb0 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -26,6 +26,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/tactic_evaluator.h"
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/pp.h"
+#include "frontends/lean/builtin_exprs.h"
 
 /* The auto quotation currently supports two classes of tactics: tactic and smt_tactic.
    To add a new class Tac, we have to
@@ -93,7 +94,10 @@ static expr mk_tactic_save_info(parser & p, pos_info const & pos, name const & t
     if (!p.env().find(save_info_name))
         throw parser_error(sstream() << "invalid tactic class '" << tac_class << "', '" <<
                            tac_class << ".save_info' has not been defined", pos);
-    return p.save_pos(mk_app(mk_constant(save_info_name), mk_prenum(mpz(pos.first)), mk_prenum(mpz(pos.second))), pos);
+    auto pos_e = mk_anonymous_constructor(mk_app(mk_expr_placeholder(),
+                                                 mk_prenum(mpz(pos.first)),
+                                                 mk_prenum(mpz(pos.second))));
+    return p.save_pos(mk_app(mk_constant(save_info_name), pos_e), pos);
 }
 
 static expr mk_tactic_solve1(parser & p, expr tac, pos_info const & pos, name const & tac_class, bool use_rstep, bool report_error) {
diff --git a/src/library/tactic/vm_monitor.cpp b/src/library/tactic/vm_monitor.cpp
index bf55e856db..2fb90eb805 100644
--- a/src/library/tactic/vm_monitor.cpp
+++ b/src/library/tactic/vm_monitor.cpp
@@ -24,6 +24,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_environment.h"
 #include "library/vm/vm_format.h"
 #include "library/vm/vm_list.h"
+#include "library/vm/vm_pos_info.h"
 #include "library/compiler/vm_compiler.h"
 #include "library/tactic/tactic_state.h"
 
@@ -216,7 +217,7 @@ vm_obj vm_decl_arity(vm_obj const & d) {
 
 vm_obj vm_decl_pos(vm_obj const & d) {
     if (optional<pos_info> pos = to_vm_decl(d).get_pos_info())
-        return mk_vm_some(mk_vm_pair(mk_vm_nat(pos->first), mk_vm_nat(pos->second)));
+        return mk_vm_some(to_obj(*pos));
     else
         return mk_vm_none();
 }
diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt
index 1caf7a147b..f7a4c77af0 100644
--- a/src/library/vm/CMakeLists.txt
+++ b/src/library/vm/CMakeLists.txt
@@ -1,4 +1,4 @@
 add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp
   vm_options.cpp vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp
   vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp vm_task.cpp
-  vm_native.cpp vm_int.cpp init_module.cpp vm_parser.cpp vm_array.cpp)
+  vm_native.cpp vm_int.cpp init_module.cpp vm_parser.cpp vm_array.cpp vm_pos_info.cpp)
diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp
index e6cc14dd92..ad70e22452 100644
--- a/src/library/vm/vm_environment.cpp
+++ b/src/library/vm/vm_environment.cpp
@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_declaration.h"
 #include "library/vm/vm_exceptional.h"
 #include "library/vm/vm_list.h"
+#include "library/vm/vm_pos_info.h"
 
 namespace lean {
 struct vm_environment : public vm_external {
@@ -203,9 +204,9 @@ vm_obj environment_decl_olean(vm_obj const & env, vm_obj const & n) {
     }
 }
 
-vm_obj environment_decl_pos_info(vm_obj const & env, vm_obj const & n) {
+vm_obj environment_decl_pos(vm_obj const & env, vm_obj const & n) {
     if (optional<pos_info> pos = get_decl_pos_info(to_env(env), to_name(n))) {
-        return mk_vm_some(mk_vm_pair(mk_vm_nat(pos->first), mk_vm_nat(pos->second)));
+        return mk_vm_some(to_obj(*pos));
     } else {
         return mk_vm_none();
     }
@@ -260,7 +261,7 @@ void initialize_vm_environment() {
     DECLARE_VM_BUILTIN(name({"environment", "symm_for"}),              environment_symm_for);
     DECLARE_VM_BUILTIN(name({"environment", "trans_for"}),             environment_trans_for);
     DECLARE_VM_BUILTIN(name({"environment", "decl_olean"}),            environment_decl_olean);
-    DECLARE_VM_BUILTIN(name({"environment", "decl_pos_info"}),         environment_decl_pos_info);
+    DECLARE_VM_BUILTIN(name({"environment", "decl_pos"}),              environment_decl_pos);
     DECLARE_VM_BUILTIN(name({"environment", "unfold_untrusted_macros"}), environment_unfold_untrusted_macros);
 }
 
diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp
index 1847e053c0..289055f025 100644
--- a/src/library/vm/vm_parser.cpp
+++ b/src/library/vm/vm_parser.cpp
@@ -20,6 +20,7 @@ Author: Sebastian Ullrich
 #include "library/vm/vm_string.h"
 #include "library/vm/vm_expr.h"
 #include "library/vm/vm_nat.h"
+#include "library/vm/vm_pos_info.h"
 #include "library/vm/interaction_state.h"
 #include "util/task_queue.h"
 
@@ -42,8 +43,7 @@ vm_obj run_parser(parser & p, expr const & spec) {
 
 vm_obj vm_parser_state_cur_pos(vm_obj const & o) {
     auto const & s = lean_parser::to_state(o);
-    auto pos = s.m_p->pos();
-    return mk_vm_pair(mk_vm_nat(pos.first), mk_vm_nat(pos.second));
+    return to_obj(s.m_p->pos());
 }
 
 vm_obj vm_parser_ident(vm_obj const & o) {
@@ -76,10 +76,10 @@ vm_obj vm_parser_qexpr(vm_obj const & vm_rbp, vm_obj const & o) {
 }
 
 void initialize_vm_parser() {
-    DECLARE_VM_BUILTIN(name({"lean", "parser_state", "cur_pos"}),  vm_parser_state_cur_pos);
-    DECLARE_VM_BUILTIN(name({"lean", "parser", "ident"}),  vm_parser_ident);
-    DECLARE_VM_BUILTIN(name({"lean", "parser", "tk"}), vm_parser_tk);
-    DECLARE_VM_BUILTIN(name({"lean", "parser", "qexpr"}),  vm_parser_qexpr);
+    DECLARE_VM_BUILTIN(name({"lean", "parser_state", "cur_pos"}), vm_parser_state_cur_pos);
+    DECLARE_VM_BUILTIN(name({"lean", "parser", "ident"}),         vm_parser_ident);
+    DECLARE_VM_BUILTIN(name({"lean", "parser", "tk"}),            vm_parser_tk);
+    DECLARE_VM_BUILTIN(name({"lean", "parser", "qexpr"}),         vm_parser_qexpr);
 }
 
 void finalize_vm_parser() {
diff --git a/src/library/vm/vm_pexpr.cpp b/src/library/vm/vm_pexpr.cpp
index 77a30fc989..f8bffff75e 100644
--- a/src/library/vm/vm_pexpr.cpp
+++ b/src/library/vm/vm_pexpr.cpp
@@ -11,10 +11,11 @@ Author: Leonardo de Moura
 #include "library/vm/vm.h"
 #include "library/vm/vm_expr.h"
 #include "library/vm/vm_string.h"
+#include "library/vm/vm_option.h"
+#include "library/vm/vm_pos_info.h"
 #include "library/quote.h"
 #include "frontends/lean/prenum.h"
 #include "library/string.h"
-#include "library/vm/vm_option.h"
 
 namespace lean {
 vm_obj pexpr_subst(vm_obj const & _e1, vm_obj const & _e2) {
@@ -51,7 +52,7 @@ vm_obj pexpr_mk_placeholder() {
 
 vm_obj pexpr_pos(vm_obj const & e) {
     if (auto p = get_pos_info(to_expr(e)))
-        return mk_vm_some(mk_vm_pair(mk_vm_nat(p->first), mk_vm_nat(p->second)));
+        return mk_vm_some(to_obj(*p));
     return mk_vm_none();
 }
 
diff --git a/src/library/vm/vm_pos_info.cpp b/src/library/vm/vm_pos_info.cpp
new file mode 100644
index 0000000000..51868d7c92
--- /dev/null
+++ b/src/library/vm/vm_pos_info.cpp
@@ -0,0 +1,18 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Sebastian Ullrich
+*/
+#include "library/vm/vm_pos_info.h"
+#include "library/vm/vm_nat.h"
+
+namespace lean {
+pos_info to_pos_info(vm_obj const & o) {
+    return {to_unsigned(cfield(o, 0)), to_unsigned(cfield(o, 1))};
+}
+
+vm_obj to_obj(pos_info p) {
+    return mk_vm_pair(mk_vm_nat(p.first), mk_vm_nat(p.second));
+}
+}
diff --git a/src/library/vm/vm_pos_info.h b/src/library/vm/vm_pos_info.h
new file mode 100644
index 0000000000..9bd0141ea5
--- /dev/null
+++ b/src/library/vm/vm_pos_info.h
@@ -0,0 +1,13 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Sebastian Ullrich
+*/
+#pragma once
+#include "library/vm/vm.h"
+
+namespace lean {
+pos_info to_pos_info(vm_obj const & o);
+vm_obj to_obj(pos_info p);
+}