From facc902a350aab168402199cd35457d907f3a6fe Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Apr 2016 19:48:42 +0200
Subject: [PATCH] Do not use internal iDestructHyp in viewshift tactics.
---
proofmode/pviewshifts.v | 42 ++++++++++++++++++++---------------------
1 file changed, 21 insertions(+), 21 deletions(-)
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 8f77deafe..f12cfd358 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -114,90 +114,90 @@ Tactic Notation "iPvsCore" constr(H) :=
end.
Tactic Notation "iPvs" open_constr(H) :=
- iPoseProof H as (fun H => iPvsCore H; last iDestructHyp H as "?").
+ iPoseProof H as (fun H => iPvsCore H; last iDestruct H as "?").
Tactic Notation "iPvs" open_constr(H) "as" constr(pat) :=
- iPoseProof H as (fun H => iPvsCore H; last iDestructHyp H as pat).
+ iPoseProof H as (fun H => iPvsCore H; last iDestruct H as pat).
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1) "}"
constr(pat) :=
- iPoseProof H as (fun H => iPvsCore H; last iDestructHyp H as { x1 } pat).
+ iPoseProof H as (fun H => iPvsCore H; last iDestruct H as { x1 } pat).
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) "}" constr(pat) :=
- iPoseProof H as (fun H => iPvsCore H; last iDestructHyp H as { x1 x2 } pat).
+ iPoseProof H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 } pat).
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
- iPoseProof H as (fun H => iPvsCore H; last iDestructHyp H as { x1 x2 x3 } pat).
+ iPoseProof H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 x3 } pat).
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
constr(pat) :=
iPoseProof H as (fun H =>
- iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 } pat).
+ iPvsCore H; last iDestruct H as { x1 x2 x3 x4 } pat).
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) "}" constr(pat) :=
iPoseProof H as (fun H =>
- iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
+ iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 } pat).
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
iPoseProof H as (fun H =>
- iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
+ iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 } pat).
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
constr(pat) :=
iPoseProof H as (fun H =>
- iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
+ iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 } pat).
Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) "}" constr(pat) :=
iPoseProof H as (fun H =>
- iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
+ iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
Tactic Notation "iPvs" open_constr(lem) constr(Hs) :=
- iPoseProof lem Hs as (fun H => iPvsCore H; last iDestructHyp H as "?").
+ iPoseProof lem Hs as (fun H => iPvsCore H; last iDestruct H as "?").
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" constr(pat) :=
- iPoseProof lem Hs as (fun H => iPvsCore H; last iDestructHyp H as pat).
+ iPoseProof lem Hs as (fun H => iPvsCore H; last iDestruct H as pat).
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) "}" constr(pat) :=
- iPoseProof lem Hs as (fun H => iPvsCore H; last iDestructHyp H as { x1 } pat).
+ iPoseProof lem Hs as (fun H => iPvsCore H; last iDestruct H as { x1 } pat).
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) simple_intropattern(x2) "}" constr(pat) :=
iPoseProof lem Hs as (fun H =>
- iPvsCore H; last iDestructHyp H as { x1 x2 } pat).
+ iPvsCore H; last iDestruct H as { x1 x2 } pat).
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) "}"
constr(pat) :=
iPoseProof lem Hs as (fun H =>
- iPvsCore H; last iDestructHyp H as { x1 x2 x3 } pat).
+ iPvsCore H; last iDestruct H as { x1 x2 x3 } pat).
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) "}" constr(pat) :=
iPoseProof lem Hs as (fun H =>
- iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 } pat).
+ iPvsCore H; last iDestruct H as { x1 x2 x3 x4 } pat).
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) "}" constr(pat) :=
iPoseProof lem Hs as (fun H =>
- iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
+ iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 } pat).
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6) "}"
constr(pat) :=
iPoseProof lem Hs as (fun H =>
- iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
+ iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 } pat).
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
simple_intropattern(x7) "}" constr(pat) :=
iPoseProof lem Hs as (fun H =>
- iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
+ iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 } pat).
Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
simple_intropattern(x7) simple_intropattern(x8) "}" constr(pat) :=
iPoseProof lem Hs as (fun H =>
- iPvsCore H; last iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
+ iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
Tactic Notation "iTimeless" constr(H) :=
match goal with
@@ -230,7 +230,7 @@ Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
apply _ || fail "iPvsAssert: " P "not a pvs"
|env_cbv; reflexivity || fail "iPvsAssert:" Hs "not found"
|env_cbv; reflexivity|
- |simpl; iDestructHyp H as pat]
+ |simpl; iDestruct H as pat]
| ?pat => fail "iPvsAssert: invalid pattern" pat
end.
Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) :=
--
GitLab