diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 05ac2922cc2b476fbfc399f2405fc033663440fd..aba95bf6c22445487b0620b8d3bd3ef23167fb29 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.