Regression in error-printing of the outline tactic #838
Description
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.