diff --git a/src/ec.ml b/src/ec.ml
index 627d25b81..c70a9dc4a 100644
--- a/src/ec.ml
+++ b/src/ec.ml
@@ -415,6 +415,7 @@ let main () =
       (*---*) gccompact   : int option;
       (*---*) docgen      : bool;
       (*---*) outdirp     : string option;
+      (*---*) upto        : (int * int option) option;
       mutable trace       : trace1 list option;
     }
 
@@ -493,6 +494,7 @@ let main () =
         ; gccompact   = None
         ; docgen      = false
         ; outdirp     = None
+        ; upto        = None
         ; trace       = None }
 
     end
@@ -511,8 +513,9 @@ let main () =
 
         let gcstats  = cmpopts.cmpo_gcstats in
         let progress = if cmpopts.cmpo_script then `Script else `Human in
+        let lastgoals = cmpopts.cmpo_lastgoals in
         let terminal =
-          lazy (T.from_channel ~name ~gcstats ~progress (open_in name))
+          lazy (T.from_channel ~name ~gcstats ~progress ~lastgoals (open_in name))
         in
 
         let trace0 =
@@ -528,6 +531,7 @@ let main () =
         ; gccompact   = cmpopts.cmpo_compact
         ; docgen      = false
         ; outdirp     = None
+        ; upto        = cmpopts.cmpo_upto
         ; trace       = trace0 }
 
       end
@@ -572,6 +576,7 @@ let main () =
         ; gccompact   = None
         ; docgen      = true
         ; outdirp     = docopts.doco_outdirp
+        ; upto        = None
         ; trace       = None }
       end
 
@@ -669,6 +674,16 @@ let main () =
   if T.interactive terminal then
     T.notice ~immediate:true `Warning copyright terminal;
 
+  (* Check if a location is past the -upto point *)
+  let past_upto (loc : EcLocation.t) =
+    match state.upto with
+    | None -> false
+    | Some (line, col) ->
+        let (sl, sc) = loc.loc_start in
+        sl > line || (sl = line && match col with
+          | None -> false
+          | Some c -> sc >= c) in
+
   try
     if T.interactive terminal then Sys.catch_break true;
 
@@ -737,6 +752,14 @@ let main () =
               List.iter
                 (fun p ->
                    let loc = p.EP.gl_action.EcLocation.pl_loc in
+
+                   (* -upto: if this command starts past the target, print goals and exit *)
+                   if past_upto loc then begin
+                     T.finalize terminal;
+                     EcCommands.pp_current_goal ~all:true Format.std_formatter;
+                     exit 0
+                   end;
+
                    let timed = p.EP.gl_debug = Some `Timed in
                    let break = p.EP.gl_debug = Some `Break in
                    let ignore_fail = ref false in
diff --git a/src/ecOptions.ml b/src/ecOptions.ml
index f012e8e8d..68b6a789e 100644
--- a/src/ecOptions.ml
+++ b/src/ecOptions.ml
@@ -26,6 +26,8 @@ and cmp_option = {
   cmpo_noeco   : bool;
   cmpo_script  : bool;
   cmpo_trace   : bool;
+  cmpo_lastgoals : bool;
+  cmpo_upto    : (int * int option) option;
 }
 
 and cli_option = {
@@ -349,6 +351,8 @@ let specs = {
       `Spec  ("script" , `Flag  , "Computer-friendly output");
       `Spec  ("no-eco" , `Flag  , "Do not cache verification results");
       `Spec  ("trace"  , `Flag  , "Save all goals & messages in .eco");
+      `Spec  ("lastgoals" , `Flag  , "Print last unproved goals on failure");
+      `Spec  ("upto"      , `String, "Compile up to LINE or LINE:COL and print goals");
       `Spec  ("compact", `Int   , "<internal>")]);
 
     ("cli", "Run EasyCrypt top-level", [
@@ -519,7 +523,14 @@ let cmp_options_of_values ini values input =
     cmpo_tstats  = get_string "tstats" values;
     cmpo_noeco   = get_flag "no-eco" values;
     cmpo_script  = get_flag "script" values;
-    cmpo_trace   = get_flag "trace" values; }
+    cmpo_trace   = get_flag "trace" values;
+    cmpo_lastgoals  = get_flag "lastgoals" values;
+    cmpo_upto       =
+      get_string "upto" values |> Option.map (fun s ->
+        match String.split_on_char ':' s with
+        | [line] -> (int_of_string line, None)
+        | [line; col] -> (int_of_string line, Some (int_of_string col))
+        | _ -> failwith "invalid -upto format: expected LINE or LINE:COL"); }
 
 let runtest_options_of_values ini values (input, scenarios) =
   { runo_input     = input;
diff --git a/src/ecOptions.mli b/src/ecOptions.mli
index 59009718a..03c69d510 100644
--- a/src/ecOptions.mli
+++ b/src/ecOptions.mli
@@ -22,6 +22,8 @@ and cmp_option = {
   cmpo_noeco   : bool;
   cmpo_script  : bool;
   cmpo_trace   : bool;
+  cmpo_lastgoals : bool;
+  cmpo_upto    : (int * int option) option;
 }
 
 and cli_option = {
diff --git a/src/ecTerminal.ml b/src/ecTerminal.ml
index 94f7c048e..de95f9238 100644
--- a/src/ecTerminal.ml
+++ b/src/ecTerminal.ml
@@ -148,8 +148,9 @@ type progress = [ `Human | `Script | `Silent ]
 class from_channel
   ?(gcstats  : bool = true)
   ?(progress : progress option)
-  ~(name     : string)
-   (stream   : in_channel)
+  ?(lastgoals : bool = false)
+  ~(name      : string)
+   (stream    : in_channel)
   : terminal
 
 = object(self)
@@ -160,6 +161,7 @@ class from_channel
   val mutable tick     = -1
   val mutable loc      = LC._dummy
   val mutable gc       = None
+  val mutable last_goals = ""
   val mutable progress =
     progress |> ofdfl (fun () ->
       if
@@ -280,7 +282,14 @@ class from_channel
 
   method finish (status : status) =
     match status with
-    | `ST_Ok -> ()
+    | `ST_Ok ->
+        if lastgoals then begin
+          let buf = Buffer.create 256 in
+          let fmt = Format.formatter_of_buffer buf in
+          EcCommands.pp_current_goal ~all:true fmt;
+          Format.pp_print_flush fmt ();
+          last_goals <- Buffer.contents buf
+        end
 
     | `ST_Failure e -> begin
         let (subloc, e) =
@@ -290,6 +299,8 @@ class from_channel
         let msg = String.strip (EcPException.tostring e) in
 
         self#_clean_progress_line ();
+        if lastgoals && last_goals <> "" then
+          Format.printf "%s%!" last_goals;
         self#_notice ?subloc ~immediate:true `Critical msg;
         self#_update_progress;
         self#_clean_progress_line ~erase:false ();
@@ -314,5 +325,5 @@ class from_channel
     Format.pp_set_margin Format.err_formatter i
 end
 
-let from_channel ?gcstats ?progress ~name stream =
-  new from_channel ?gcstats ?progress ~name stream
+let from_channel ?gcstats ?progress ?lastgoals ~name stream =
+  new from_channel ?gcstats ?progress ?lastgoals ~name stream
diff --git a/src/ecTerminal.mli b/src/ecTerminal.mli
index 0a96a56d2..faacff0e7 100644
--- a/src/ecTerminal.mli
+++ b/src/ecTerminal.mli
@@ -22,6 +22,7 @@ type progress = [ `Human | `Script | `Silent ]
 val from_channel :
      ?gcstats:bool
   -> ?progress:progress
+  -> ?lastgoals:bool
   -> name:string
   -> in_channel
   -> terminal