From 09741a0349b9746daa429652fc8e91d674caee2b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Dec 2017 12:09:33 +0100
Subject: [PATCH] Comment on the `uPred` module trick.

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

diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 05ac2922c..aba95bf6c 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -1,6 +1,9 @@
 From iris.base_logic Require Export derived.
 Set Default Proof Using "Type".
 
+(* The trick of having multiple [uPred] modules, which are all exported in
+another [uPred] module is by Jason Gross and described in:
+https://sympa.inria.fr/sympa/arc/coq-club/2016-12/msg00069.html *)
 Module Import uPred.
   Export upred.uPred.
   Export primitive.uPred.
-- 
GitLab