From 1520e6a5b5e791fe6f8ff8f07e839999b7c92c9f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 10 Sep 2020 21:46:08 +0200
Subject: [PATCH] Clean up error handling code `iApply`.
The old code contained a bunch of unused spaghetti that was not cleaned up
after a refactoring.
@jihgfee menaged to trigger a wrong code path in the old code, but I failed
to turn his test case into a self-contained one.
---
theories/proofmode/ltac_tactics.v | 15 ++++++---------
1 file changed, 6 insertions(+), 9 deletions(-)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 92d12aacd..2a4018986 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1157,15 +1157,12 @@ premises [n], the tactic will have the following behavior:
0 if we should proceed to the [n > 0] case, and with level 1 if there is an
actual error. *)
Local Ltac iApplyHypExact H :=
- first
- [eapply tac_assumption with H _ _; (* (i:=H) *)
- [pm_reflexivity || fail 1
- |iSolveTC || fail 1
- |pm_reduce; iSolveTC]
- |lazymatch iTypeOf H with
- | Some (_,?Q) =>
- fail 2 "iApply: remaining hypotheses not affine and the goal not absorbing"
- end].
+ eapply tac_assumption with H _ _; (* (i:=H) *)
+ [pm_reflexivity
+ |iSolveTC
+ |pm_reduce; iSolveTC ||
+ fail 1 "iApply: remaining hypotheses not affine and the goal not absorbing"].
+
Local Ltac iApplyHypLoop H :=
first
[eapply tac_apply with H _ _ _;
--
GitLab