Commit a051dd3c authored by Robbert Krebbers's avatar Robbert Krebbers

Make `iEval` fail in case it is not a proof mode goal.

parent 467b118b
......@@ -82,8 +82,8 @@ Ltac iStartProof :=
(** * Simplification *)
Tactic Notation "iEval" tactic(t) :=
try iStartProof;
try (eapply tac_eval; [t; reflexivity|]).
iStartProof;
eapply tac_eval; [t; reflexivity|].
Tactic Notation "iSimpl" := iEval simpl.
......
Markdown is supported
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