From 66483b1db4023e36049a5ed10dc7e9222c97ee6b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Oct 2018 01:14:43 +0200
Subject: [PATCH] A comment explaining the `invG` submodule.

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

diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index d8f06c6d3..ccd63aa52 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -4,6 +4,9 @@ From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
+(** All definitions in this file are internal to [fancy_updates] with the
+exception of what's in the [invG] module. The module [invG] is thus exported in
+[fancy_updates], which [wsat] is only imported. *)
 Module invG.
   Class invG (Î£ : gFunctors) : Set := WsatG {
     inv_inG :> inG Î£ (authR (gmapUR positive (agreeR (laterC (iPreProp Î£)))));
-- 
GitLab