From 1eba71212e062b16f70cdde87687fc44458432f1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 27 Nov 2017 09:07:53 +0100
Subject: [PATCH] Add comment.

---
 theories/program_logic/ectx_language.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 3c20309d3..9f00ed60a 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -216,6 +216,13 @@ End ectx_language.
 Arguments ectx_lang : clear implicits.
 Coercion ectx_lang : ectxLanguage >-> language.
 
+(* This definition makes sure that the fields of the [language] record do not
+refer to the projections of the [ectxLanguage] record but to the actual fields
+of the [ectxLanguage] record. This is crucial for canonical structure search to
+work.
+
+Note that this trick no longer works when we switch to canonical projections
+because then the pattern match [let '...] will be desugared into projections. *)
 Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
   let '@EctxLanguage E V C St of_val to_val empty comp fill head mix := Λ in
   @Language E V St of_val to_val _
-- 
GitLab