diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index 62d1b3d6d0b89df583506305eaece9ee1389bf0b..75ea52bef9f13ad4486746b4bac00e28441ba0d6 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -2,8 +2,7 @@ From iris.heap_lang Require Export lang.
 Import heap_lang.
 
 (** The tactic [simpl_subst] performs substitutions in the goal. Its behavior
-can be tuned using instances of the type class [Closed e], which can be used
-to mark that expressions are closed, and should thus not be substituted into. *)
+can be tuned by declaring [WExpr] and [WSubst] instances. *)
 
 (** * Weakening *)
 Class WExpr {X Y} (H : X `included` Y) (e : expr X) (er : expr Y) :=