diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v index 25e1a364bf56c7a05f8f66cdb71e223073554e63..0dd09eebe82e594177b8556d8504380fd7832a97 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.