diff --git a/program_logic/ectx_language.v b/program_logic/ectx_language.v
index 2cae45d149b7270ae8508dfd1f035dea5350e9d3..8e9fa62e8d1a97f50ab7598e0cb0919e94c26273 100644
--- a/program_logic/ectx_language.v
+++ b/program_logic/ectx_language.v
@@ -1,3 +1,5 @@
+(** An axiomatization of evaluation-context based languages, including a proof
+    that this gives rise to a "language" in the Iris sense. *)
 From iris.algebra Require Export base.
 From iris.program_logic Require Export language.
 
diff --git a/program_logic/ectx_weakestpre.v b/program_logic/ectx_weakestpre.v
index c28eff3f4d02e8288cec0bca1375c2d09a90b4d8..820ff411a3589dd721b4de1954368ade0870bb11 100644
--- a/program_logic/ectx_weakestpre.v
+++ b/program_logic/ectx_weakestpre.v
@@ -1,3 +1,4 @@
+(** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
 From iris.program_logic Require Import ownership.