From 5703969d3ce38097388458f70b435e716899abbc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Feb 2021 13:09:21 +0100
Subject: [PATCH] clarify Pmap_raw comment

---
 theories/pmap.v | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/theories/pmap.v b/theories/pmap.v
index f4a185a5..a6630209 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -15,10 +15,11 @@ Local Hint Extern 0 (_ =@{positive} _) => congruence : core.
 Local Hint Extern 0 (_ ≠@{positive} _) => congruence : core.
 
 (** * The tree data structure *)
-(** The data type [Pmap_raw] specifies radix-2 search trees. These trees do
-not ensure canonical representations of maps. For example the empty map can
-be represented as a binary tree of an arbitrary size that contains [None] at
-all nodes. *)
+(** The internal data type [Pmap_raw] specifies radix-2 search trees. These
+trees do not ensure canonical representations of maps. For example the empty map
+can be represented as a binary tree of an arbitrary size that contains [None] at
+all nodes.
+See below for [Pmap] which ensures canonical representation. *)
 Inductive Pmap_raw (A : Type) : Type :=
   | PLeaf: Pmap_raw A
   | PNode: option A → Pmap_raw A → Pmap_raw A → Pmap_raw A.
-- 
GitLab