From 7adcba8fb9d93ad76b117a03484ba72a974e93e7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 21 Nov 2019 11:43:37 +0100
Subject: [PATCH] add a comment to final erasure theorem

---
 theories/heap_lang/proph_erasure.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/heap_lang/proph_erasure.v b/theories/heap_lang/proph_erasure.v
index 6f0be275e..6f3f155c3 100644
--- a/theories/heap_lang/proph_erasure.v
+++ b/theories/heap_lang/proph_erasure.v
@@ -741,6 +741,7 @@ Proof.
   - right; eauto using reducible_no_obs_reducible.
 Qed.
 
+(** This is the top-level erasure theorem: erasure preserves adequacy. *)
 Theorem erasure e σ φ :
   adequate NotStuck e σ φ →
   adequate NotStuck (erase_expr e) (erase_state σ)
-- 
GitLab