From da56bbb0f26f4f77fe28efea60f81f06d8a2ac59 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 23 Jan 2017 17:16:24 +0100
Subject: [PATCH] Unused premises go to the last premise of iApply (instead of
the first).
---
ProofMode.md | 4 ++--
theories/proofmode/tactics.v | 2 +-
theories/tests/proofmode.v | 2 +-
3 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/ProofMode.md b/ProofMode.md
index e004d3595..b17ec1fc6 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -17,8 +17,8 @@ Applying hypotheses and lemmas
conclusion of `pm_trm` and generates goals for the premises of `pm_trm`. See
proof mode terms below.
If the applied term has more premises than given specialization patterns, the
- pattern is extended with `[-] ... [-]`. As a consequence, all unused spatial
- hypotheses move to the first premise without an explicit specialization
+ pattern is extended with `[] ... []`. As a consequence, all unused spatial
+ hypotheses move to the last premise without an explicit specialization
pattern.
Context management
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index af482f59e..a5f79c5fe 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -431,7 +431,7 @@ Tactic Notation "iApply" open_constr(lem) :=
[env_cbv; reflexivity
|apply _
|lazy beta (* reduce betas created by instantiation *)]
- |iSpecializePat H "[-]"; last go H] in
+ |iSpecializePat H "[]"; last go H] in
iPoseProofCore lem as false true (fun H =>
first [iExact H|go H|iTypeOf H (fun Q => fail 1 "iApply: cannot apply" Q)]).
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index f8302508d..28e5da973 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -118,5 +118,5 @@ Proof.
Qed.
Lemma demo_11 (M : ucmraT) (P Q R : uPred M) :
- (P -∗ Q -∗ True -∗ True -∗ R) -∗ P -∗ Q -∗ R.
+ (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R.
Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed.
--
GitLab