Commit 7dbf98f4 authored by Robbert Krebbers's avatar Robbert Krebbers

Update comment in substitution.v.

parent 6d43651e
Pipeline #935 passed with stage
......@@ -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) :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment