From 753de83ec64f4255c34a85a0fc5e381338524fb9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 18 Feb 2018 10:31:20 +0100
Subject: [PATCH] Fix error message of `iMod`
Thanks to @jtassaro for reporting this problem.
---
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 18c780e64..ade36115e 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -969,8 +969,8 @@ Tactic Notation "iModCore" constr(H) :=
eapply tac_modal_elim with _ H _ _ _ _ _;
[env_reflexivity || fail "iMod:" H "not found"
|apply _ ||
- let P := match goal with |- ElimModal ?P _ _ _ => P end in
- let Q := match goal with |- ElimModal _ _ ?Q _ => Q end in
+ let P := match goal with |- ElimModal _ ?P _ _ _ => P end in
+ let Q := match goal with |- ElimModal _ _ _ ?Q _ => Q end in
fail "iMod: cannot eliminate modality " P "in" Q
|try fast_done (* optional side-condition *)
|env_reflexivity|].
--
GitLab