diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 40277672d4a238e346fac91e236ce8e8c01349c1..2dbf8cecdb91ac597bebac8065b8948bcb858eac 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -109,14 +109,16 @@ Ltac iElaborateSelPat pat :=
     let pat := sel_pat.parse pat in go pat Δ (@nil esel_pat)
   end.
 
+Local Ltac iClearHyp H :=
+  eapply tac_clear with _ H _ _; (* (i:=H) *)
+    [env_reflexivity || fail "iClear:" H "not found"|].
+
 Tactic Notation "iClear" constr(Hs) :=
   let rec go Hs :=
     lazymatch Hs with
     | [] => idtac
     | ESelPure :: ?Hs => clear; go Hs
-    | ESelName _ ?H :: ?Hs =>
-       eapply tac_clear with _ H _ _; (* (i:=H) *)
-         [env_reflexivity || fail "iClear:" H "not found"|go Hs]
+    | ESelName _ ?H :: ?Hs => iClearHyp H; go Hs
     end in
   let Hs := iElaborateSelPat Hs in go Hs.
 
@@ -845,8 +847,8 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
   let rec go Hz pat :=
     lazymatch pat with
     | IAnom => idtac
-    | IDrop => iClear Hz
-    | IFrame => iFrame Hz
+    | IDrop => iClearHyp Hz
+    | IFrame => iFrameHyp Hz
     | IName ?y => iRename Hz into y
     | IList [[]] => iExFalso; iExact Hz
     | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; go Hz pat1