From 720536fa02f6ddad860b15558c83088e96d5d99a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 5 Jan 2017 13:54:17 +0100
Subject: [PATCH] document base_logic.upred

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

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 944e5de7f..c10ca5967 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,6 +1,11 @@
 From iris.algebra Require Export cmra.
 Set Default Proof Using "Type*".
 
+(** The basic definition of the uPred type, its metric and functor laws.
+    You probably do not want to import this file. Instead, import
+    base_logic.base_logic; that will also give you all the primitive
+    and many derived laws for the logic. *)
+
 Record uPred (M : ucmraT) : Type := IProp {
   uPred_holds :> nat → M → Prop;
   uPred_mono n x1 x2 : uPred_holds n x1 → x1 ≼{n} x2 → uPred_holds n x2;
-- 
GitLab