From 22b866173a8d6e6964f820f6c964fe79f938ba2e Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Sat, 16 Jan 2021 12:56:42 +0100
Subject: [PATCH] some comments

---
 theories/typing/contextual_refinement.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index 7498009..669627a 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 →
-- 
GitLab