Regression in error-printing of the `outline` tactic

[loutr]

Commit 23cf445 introduced a regression on error-printing for the outline tactic. Before, an error-message was displayed if the code positions were wrong. Now the tactic fails with an anomaly. The behaviour of the tactic whenever the code position is correct remains unaffected.

type t.
op (+) : t -> t -> t.

module M = {
  proc f(x) = {
    var y;
    y <- x + x;
    return y;
  }

  proc g(x) = {
    var z, y, r;
    z <- x;

    y <- x + x;
    r <- y;
    return z + r;
  }
  
  proc h(x) = {
    var z, y;
    z <- x;
    y <@ f(x);
    return z + y;
  }
}.

equiv example : M.g ~ M.h : ={arg} ==> ={res}.
proof.
proc.
outline{1} 3 M.f. (* instead of [2-3] *)
(* before:
     Outline: body's are different lengths
     y <- x{hr} + x{hr}; ~ . *)
(* after:
     Failure("expecting memory") *)
admitted.