Commit facc902a authored by Robbert Krebbers's avatar Robbert Krebbers

Do not use internal iDestructHyp in viewshift tactics.

parent c399acaf
...@@ -114,90 +114,90 @@ Tactic Notation "iPvsCore" constr(H) := ...@@ -114,90 +114,90 @@ Tactic Notation "iPvsCore" constr(H) :=
end. end.
Tactic Notation "iPvs" open_constr(H) := 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) := 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) "}" Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1) "}"
constr(pat) := 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) Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) "}" constr(pat) := 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) Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) := 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) Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}" simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
constr(pat) := constr(pat) :=
iPoseProof H as (fun H => 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) Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) "}" constr(pat) := simple_intropattern(x5) "}" constr(pat) :=
iPoseProof H as (fun H => 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) Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) := simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
iPoseProof H as (fun H => 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) Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}" simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
constr(pat) := constr(pat) :=
iPoseProof H as (fun H => 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) Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) "}" constr(pat) := simple_intropattern(x8) "}" constr(pat) :=
iPoseProof H as (fun H => 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) := 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) := 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" "{" Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) "}" constr(pat) := 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" "{" Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) simple_intropattern(x2) "}" constr(pat) := simple_intropattern(x1) simple_intropattern(x2) "}" constr(pat) :=
iPoseProof lem Hs as (fun H => 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" "{" Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) "}" simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) "}"
constr(pat) := constr(pat) :=
iPoseProof lem Hs as (fun H => 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" "{" Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) "}" constr(pat) := simple_intropattern(x4) "}" constr(pat) :=
iPoseProof lem Hs as (fun H => 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" "{" Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) "}" constr(pat) := simple_intropattern(x4) simple_intropattern(x5) "}" constr(pat) :=
iPoseProof lem Hs as (fun H => 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" "{" Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6) "}" simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6) "}"
constr(pat) := constr(pat) :=
iPoseProof lem Hs as (fun H => 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" "{" Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
simple_intropattern(x7) "}" constr(pat) := simple_intropattern(x7) "}" constr(pat) :=
iPoseProof lem Hs as (fun H => 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" "{" Tactic Notation "iPvs" open_constr(lem) constr(Hs) "as" "{"
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
simple_intropattern(x7) simple_intropattern(x8) "}" constr(pat) := simple_intropattern(x7) simple_intropattern(x8) "}" constr(pat) :=
iPoseProof lem Hs as (fun H => 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) := Tactic Notation "iTimeless" constr(H) :=
match goal with match goal with
...@@ -230,7 +230,7 @@ Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) "with" constr(Hs) := ...@@ -230,7 +230,7 @@ Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
apply _ || fail "iPvsAssert: " P "not a pvs" apply _ || fail "iPvsAssert: " P "not a pvs"
|env_cbv; reflexivity || fail "iPvsAssert:" Hs "not found" |env_cbv; reflexivity || fail "iPvsAssert:" Hs "not found"
|env_cbv; reflexivity| |env_cbv; reflexivity|
|simpl; iDestructHyp H as pat] |simpl; iDestruct H as pat]
| ?pat => fail "iPvsAssert: invalid pattern" pat | ?pat => fail "iPvsAssert: invalid pattern" pat
end. end.
Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) := Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) :=
......
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