Commit 1f3e92e3 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso

Fix inconsistent invocation of iPoseProofCoreLem

The parens are inconsistent with the other call to `iPoseProofCoreLem`, and this
will break after switching to tactic3.
parent e47c73d8
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment