From 7dbf98f4912fa10d45ee884fd4f5fc24b80492e2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 10 May 2016 21:12:02 +0200
Subject: [PATCH] Update comment in substitution.v.
---
heap_lang/substitution.v | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index 62d1b3d6d..75ea52bef 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) :=
--
GitLab