From a051dd3cd6cfc5d1683ce13639aa128385e1c267 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 31 Dec 2017 18:28:28 +0100
Subject: [PATCH] Make `iEval` fail in case it is not a proof mode goal.

---
 theories/proofmode/tactics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 25e1a364b..0dd09eebe 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -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.
 
-- 
GitLab