Better error message for iAlways.

272535e4 · Robbert Krebbers · 83184356 · 272535e4
Commit 272535e4 authored Aug 04, 2017 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 1 deletion

theories/proofmode/tactics.v theories/proofmode/tactics.v +2 -1

No files found.
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -778,7 +778,8 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Always *)
 Tactic Notation "iAlways":=
  iStartProof;
-  apply tac_always_intro; env_cbv.
+  apply tac_always_intro; env_cbv
+    || fail "iAlways: the goal is not an always modality".

 (** * Later *)
 Tactic Notation "iNext" open_constr(n) :=