diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 0d99ef960f2a98643342024006ffebe8a81df446..5c7637c9ca212ee9d787d67e973c6f2f6b69e60c 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -676,7 +676,7 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
   let rec find_pat found pats :=
     lazymatch pats with
     | [] =>
-      match found with
+      lazymatch found with
       | true => idtac
       | false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
       end
@@ -684,7 +684,7 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
     | IClear ?H :: ?pats => iClear H; find_pat found pats
     | IClearFrame ?H :: ?pats => iFrame H; find_pat found pats
     | ?pat :: ?pats =>
-       match found with
+       lazymatch found with
        | false => go H pat; find_pat true pats
        | true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
        end