some comments

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 →