diff --git a/ProofMode.md b/ProofMode.md
index de5340bf9e56b90b42f1f82755f74cfca2be7876..74e0b0d1db1483754622fd1ca701d6a1bc2dd485 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -23,8 +23,9 @@ Context management
 - `iIntros (x1 ... xn) "ipat1 ... ipatn"` : introduce universal quantifiers
   using Coq introduction patterns `x1 ... xn` and implications/wands using proof
   mode introduction patterns `ipat1 ... ipatn`.
-- `iClear "H1 ... Hn"` : clear the hypothesis `H1 ... Hn`. The symbol `★` can
-  be used to clear entire spatial context.
+- `iClear (x1 ... xn) "H1 ... Hn"` : clear the hypothesis `H1 ... Hn` as well as
+  the Coq level hypotheses/variables `x1 ... xn`. The symbol `★` can be used to
+  clear entire spatial context.
 - `iRevert (x1 ... xn) "H1 ... Hn"` : revert the proof mode hypotheses
   `H1 ... Hn` into wands, as well as the Coq level hypotheses/variables
   `x1 ... xn` into universal quantifiers. The symbol `★` can be used to revert
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 1fabcf66a2e843aea8c2e89615f493139952b689..7ee2bb6ebc963a9666cf8c74d78c7075bd8716eb 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -66,6 +66,8 @@ Tactic Notation "iClear" constr(Hs) :=
          [env_cbv; reflexivity || fail "iClear:" H "not found"|go Hs]
     end in
   let Hs := words Hs in go Hs.
+Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
+  iClear Hs; clear xs.
 
 (** * Assumptions *)
 Tactic Notation "iExact" constr(H) :=