Commit a155cf62 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Better error message for iTimeless.

This solves issue 33.
parent c99ab2e5
...@@ -522,7 +522,7 @@ Tactic Notation "iTimeless" constr(H) := ...@@ -522,7 +522,7 @@ Tactic Notation "iTimeless" constr(H) :=
apply _ || fail "iTimeless: cannot remove later when goal is" Q apply _ || fail "iTimeless: cannot remove later when goal is" Q
|env_cbv; reflexivity || fail "iTimeless:" H "not found" |env_cbv; reflexivity || fail "iTimeless:" H "not found"
|let P := match goal with |- IntoExceptLast ?P _ => P end in |let P := match goal with |- IntoExceptLast ?P _ => P end in
apply _ || fail "iTimeless:" P "not timeless" apply _ || fail "iTimeless: cannot turn" P "into ◇"
|env_cbv; reflexivity|]. |env_cbv; reflexivity|].
(** * View shifts *) (** * View shifts *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment