diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index 74980093bc13dfbabfa8a75f0d4a3cb03f9849e3..669627a6b0497c0ea984731c213dd00c3ad771cf 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -242,6 +242,9 @@ Inductive typed_ctx: ctx → stringmap type → type → stringmap type → type
      typed_ctx K Γ1 τ1 Γ2 τ2 →
      typed_ctx (k :: K) Γ1 τ1 Γ3 τ3.
 
+(** The main definition of contextual refinement that we use. An
+    alternative (equivalent) formulation which observes only
+    termination can be found in [contextual_refinement_alt.v] *)
 Definition ctx_refines (Γ : stringmap type)
     (e e' : expr) (τ : type) : Prop := ∀ K thp σ₀ σ₁ (b : bool),
   typed_ctx K Γ τ ∅ TBool →