From 1f3e92e30b8f44693025f4d4cb6ba7ef7912105f Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 14 Jun 2019 18:15:39 +0200
Subject: [PATCH] Fix inconsistent invocation of iPoseProofCoreLem
The parens are inconsistent with the other call to `iPoseProofCoreLem`, and this
will break after switching to tactic3.
---
theories/proofmode/ltac_tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 2d055b316..41293ccd0 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1032,7 +1032,7 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
| true =>
iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
| false =>
- iPoseProofCoreLem t as Htmp before_tc (spec_tac ()); [..|tac Htmp]
+ iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
end
end.
--
GitLab