diff --git a/library/init/meta/vm.lean b/library/init/meta/vm.lean
index 8cc5760bed..d1599c434d 100644
--- a/library/init/meta/vm.lean
+++ b/library/init/meta/vm.lean
@@ -16,16 +16,29 @@ inductive vm_obj_kind
 
 namespace vm_obj
 meta constant kind            : vm_obj → vm_obj_kind
+/- For simple and constructor vm_obj's, it returns the constructor tag/index.
+   Return 0 otherwise. -/
 meta constant cidx            : vm_obj → nat
+/- For closure vm_obj's, it returns the internal function index. -/
 meta constant fn_idx          : vm_obj → nat
+/- For constructor vm_obj's, it returns the data stored in the object.
+   For closure vm_obj's, it returns the local arguments captured by the closure. -/
 meta constant fields          : vm_obj → list vm_obj
+/- For simple and mpz vm_obj's -/
 meta constant to_nat          : vm_obj → nat
+/- For name vm_obj's, it returns the name wrapped by the vm_obj. -/
 meta constant to_name         : vm_obj → name
+/- For level vm_obj's, it returns the universe level wrapped by the vm_obj. -/
 meta constant to_level        : vm_obj → level
+/- For expr vm_obj's, it returns the expression wrapped by the vm_obj. -/
 meta constant to_expr         : vm_obj → expr
+/- For declaration vm_obj's, it returns the declaration wrapped by the vm_obj. -/
 meta constant to_declaration  : vm_obj → declaration
+/- For environment vm_obj's, it returns the environment wrapped by the vm_obj. -/
 meta constant to_environment  : vm_obj → environment
+/- For tactic_state vm_obj's, it returns the tactic_state object wrapped by the vm_obj. -/
 meta constant to_tactic_state : vm_obj → tactic_state
+/- For format vm_obj's, it returns the format object wrapped by the vm_obj. -/
 meta constant to_format       : vm_obj → format
 end vm_obj
 
@@ -34,16 +47,23 @@ meta constant vm_decl : Type
 inductive vm_decl_kind
 | bytecode | builtin | cfun
 
-structure vm_local_info :=
-(id : name) (pos : option (nat × nat))
+/- Information for local variables and arguments on the VM stack.
+   Remark: type is only available if it is a closed term at compilation time. -/
+meta structure vm_local_info :=
+(id : name) (type : option expr)
 
 namespace vm_decl
 meta constant kind      : vm_decl → vm_decl_kind
 meta constant to_name   : vm_decl → name
+/- Internal function index associated with the given VM declaration. -/
 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 .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. -/
 meta constant args_info : vm_decl → list vm_local_info
 end vm_decl
 
@@ -62,20 +82,42 @@ meta constant get_env              : vm environment
 meta constant get_decl             : name → vm vm_decl
 meta constant get_options          : vm options
 meta constant stack_size           : vm nat
+/- Return the vm_obj stored at the given position on the execution stack.
+   It fails if position >= vm.stack_size -/
 meta constant stack_obj            : nat → vm vm_obj
+/- Return (name, type) for the object at the given position on the execution stack.
+   It fails if position >= vm.stack_size.
+   The name is anonymous if vm_obj is a transient value created by the compiler.
+   Type information is only recorded if the type is a closed term at compilation time. -/
 meta constant stack_obj_info       : nat → vm (name × option expr)
+/- Pretty print the vm_obj at the given position on the execution stack. -/
 meta constant pp_stack_obj         : nat → vm format
+/- Pretty print the given expression. -/
 meta constant pp_expr              : expr → vm format
+/- Number of frames on the call stack. -/
 meta constant call_stack_size      : vm nat
+/- Return the function name at the given stack frame.
+   Action fails if position >= vm.call_stack_size. -/
 meta constant call_stack_fn        : nat → vm name
+/- Return the range [start, end) for the given stack frame.
+   Action fails if position >= vm.call_stack_size.
+   The values start and end correspond to positions at the execution stack.
+   We have that 0 <= start < end <= vm.stack_size -/
 meta constant call_stack_var_range : nat → vm (nat × nat)
+/- Return the name of the function on top of the call stack. -/
 meta constant curr_fn              : vm name
+/- Return the base stack pointer for the frame on top of the call stack. -/
 meta constant bp                   : vm nat
+/- Return the program counter. -/
 meta constant pc                   : vm nat
+/- Convert the given vm_obj into a string -/
 meta constant obj_to_string        : vm_obj → vm string
 meta constant put_str              : string → vm unit
 meta constant get_line             : vm string
+/- Return tt if end of the input stream has been reached.
+   For example, this can happen if the user presses Ctrl-D -/
 meta constant eof                  : vm bool
+/- Return the list of declarations tagged with the given attribute. -/
 meta constant get_attribute        : name → vm (list name)
 
 meta def trace {A : Type} [has_to_format A] (a : A) : vm unit :=
@@ -88,5 +130,8 @@ meta structure vm_monitor (s : Type) :=
 (init : s) (step : s → vm s)
 
 /- Registers a new virtual machine monitor. The argument must be the name of a definition of type
-   `vm_monitor S`. The command will override the last monitor. -/
+   `vm_monitor S`. The command will override the last monitor.
+
+   If option 'debugger' is true, then the VM will initialize the vm_monitor state using the
+   'init' field, and will invoke the function 'step' before each instruction is invoked. -/
 meta constant vm_monitor.register : name → command
diff --git a/tmp/cli_debugger.lean b/tmp/cli_debugger.lean
index 27249bab43..a89b7223b4 100644
--- a/tmp/cli_debugger.lean
+++ b/tmp/cli_debugger.lean
@@ -61,16 +61,16 @@ do {
 <|>
 return "<position not available>"
 
-meta def display_fn (header : string) (fn : name) (frame : nat) : vm unit :=
+meta def show_fn (header : string) (fn : name) (frame : nat) : vm unit :=
 do pos ← pos_info fn,
    vm.put_str ("[" ++ frame^.to_string ++ "] " ++ header ++ " " ++ fn^.to_string ++ " at " ++ pos ++ "\n")
 
-meta def display_curr_fn (header : string) : vm unit :=
+meta def show_curr_fn (header : string) : vm unit :=
 do fn ← vm.curr_fn,
    sz ← vm.call_stack_size,
-   display_fn header fn (sz-1)
+   show_fn header fn (sz-1)
 
-meta def display_help : vm unit :=
+meta def show_help : vm unit :=
 do
  vm.put_str "exit      - stop debugger\n",
  vm.put_str "help      - display this message\n",
@@ -80,6 +80,7 @@ do
  vm.put_str " up        - move up in the stack trace\n",
  vm.put_str " down      - move down in the stack trace\n",
  vm.put_str " vars      - display variables in the current stack frame\n",
+ vm.put_str " stack     - display all functions on the call stack\n",
  vm.put_str "breakpoints\n",
  vm.put_str " break fn  - add breakpoint for fn\n",
  vm.put_str " rbreak fn - remove breakpoint\n",
@@ -128,7 +129,7 @@ meta def show_breakpoints : list name → vm unit
 meta def show_frame (frame : nat) : vm unit :=
 do sz ← vm.call_stack_size,
    fn ← if frame >= sz then vm.curr_fn else vm.call_stack_fn frame,
-   display_fn "frame" fn frame
+   show_fn "frame" fn frame
 
 meta def up (frame : nat) : vm nat :=
 if frame = 0 then return 0
@@ -175,6 +176,17 @@ meta def show_vars (frame : nat) : vm unit :=
 do (s, e) ← vm.call_stack_var_range frame,
    show_vars_core 0 s e
 
+meta def show_stack_core : nat → vm unit
+| 0     := return ()
+| (i+1) := do
+  fn ← vm.call_stack_fn i,
+  show_fn "stack" fn i,
+  show_stack_core i
+
+meta def show_stack : vm unit :=
+do sz ← vm.call_stack_size,
+   show_stack_core sz
+
 meta def cmd_loop_core : state → nat → list string → vm state
 | s frame default_cmd := do
   is_eof ← vm.eof,
@@ -189,7 +201,7 @@ meta def cmd_loop_core : state → nat → list string → vm state
     match tks with
     | []          := cmd_loop_core s frame default_cmd
     | (cmd::args) :=
-      if cmd = "help" then display_help >> cmd_loop_core s frame default_cmd
+      if cmd = "help" then show_help >> cmd_loop_core s frame default_cmd
       else if cmd = "exit" then return {s with md := mode.done }
       else if cmd = "run" ∨ cmd = "r" then return {s with md := mode.run }
       else if cmd = "step" ∨ cmd = "s" then return {s with md := mode.step }
@@ -201,7 +213,8 @@ meta def cmd_loop_core : state → nat → list string → vm state
         cmd_loop_core s frame default_cmd
       else if cmd = "up" ∨ cmd = "u" then do frame ← up frame, cmd_loop_core s frame ["u"]
       else if cmd = "down" ∨ cmd = "d" then do frame ← down frame, cmd_loop_core s frame ["d"]
-      else if cmd = "vars" ∨ cmd = "v" then do show_vars frame, cmd_loop_core s frame ["vars"]
+      else if cmd = "vars" ∨ cmd = "v" then do show_vars frame, cmd_loop_core s frame []
+      else if cmd = "stack" then do show_stack, cmd_loop_core s frame []
       else do vm.put_str "unknown command, type 'help' for help\n", cmd_loop_core s frame default_cmd
     end
 
@@ -231,7 +244,7 @@ do opts ← vm.get_options,
        return {new_s with md := mode.run}
      else do
        vm.put_str "Lean debugger\n",
-       display_curr_fn "debugging",
+       show_curr_fn "debugging",
        vm.put_str "type 'help' for help\n",
        cmd_loop new_s []
 
@@ -240,7 +253,7 @@ do
   sz ← vm.call_stack_size,
   if sz = s^.csz then return s
   else do
-    display_curr_fn "step",
+    show_curr_fn "step",
     cmd_loop s ["s"]
 
 meta def bp_reached (s : state) : vm bool :=
@@ -259,7 +272,7 @@ do b1 ← in_active_bps s,
    b2 ← bp_reached s,
    if b1 ∨ not b2 then return s
    else do
-     display_curr_fn "breakpoint",
+     show_curr_fn "breakpoint",
      fn    ← vm.curr_fn,
      sz    ← vm.call_stack_size,
      new_s ← return $ {s with active_bps := (sz, fn) :: s^.active_bps},