From 552f906a797745559cd3f96328cf9c0ce584c3ea Mon Sep 17 00:00:00 2001
From: Darius Foo <darius.foo.tw@gmail.com>
Date: Wed, 19 Jul 2023 13:42:55 +0800
Subject: [PATCH] Add note on pure frame

---
 parsing/entail.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/parsing/entail.ml b/parsing/entail.ml
index f56b4451..f5e180bf 100644
--- a/parsing/entail.ml
+++ b/parsing/entail.ml
@@ -400,6 +400,7 @@ let rec check_staged_subsumption_stagewise :
           fail)
         else ok
       in
+      (* pure information propagates forward across stages, not heap info *)
       let* residue =
         let arg_eqs = conj (List.map2 (fun x y -> Atomic (EQ, x, y)) a1 a2) in
         stage_subsumes ctx