diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 754ba2e5535d8821ae53639e18927af75064871a..1fabcf66a2e843aea8c2e89615f493139952b689 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -58,7 +58,7 @@ Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
 
 Tactic Notation "iClear" constr(Hs) :=
   let rec go Hs :=
-    match Hs with
+    lazymatch Hs with
     | [] => idtac
     | "★" :: ?Hs => eapply tac_clear_spatial; [env_cbv; reflexivity|go Hs]
     | ?H :: ?Hs =>