diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 8f77deafe28c52097d0808a47e3234e8325d3e85..f12cfd3585849628deaeca7cc20b032bda77a529 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) :=