From 296dc646408ae23c9c6f836275684722e70db1fc Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Thu, 3 Dec 2020 10:19:38 +0100
Subject: [PATCH] Add comment documenting the dfrac notation

---
 iris/algebra/dfrac.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index 768f688b8..a73b968c4 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -32,6 +32,10 @@ Inductive dfrac :=
   | DfracDiscarded : dfrac
   | DfracBoth : Qp → dfrac.
 
+(* This notation is intended to be used as a component in other notations that
+   include discardable fractions. The notation provides shorthands for the
+   constructors and the commonly used full fraction. For and example
+   demonstrating how this can be used see the notation in [gen_heap.v]. *)
 Declare Custom Entry dfrac.
 Notation "{ dq }" := (dq) (in custom dfrac at level 1, dq constr).
 Notation "â–¡" := DfracDiscarded (in custom dfrac).
-- 
GitLab