From 3b269ef3b688ca88a2360969b0e936cbe50f2bcb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 18 Feb 2025 07:29:37 +0000
Subject: [PATCH] improve comment

---
 stdpp/countable.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/stdpp/countable.v b/stdpp/countable.v
index ebcd0f93..73993ceb 100644
--- a/stdpp/countable.v
+++ b/stdpp/countable.v
@@ -315,13 +315,16 @@ Local Close Scope positive.
 
 (** This type can help you construct a [Countable] instance for an arbitrary
 (even recursive) inductive datatype. The idea is tht you make [T] something like
-`T1 + T2 + ...`, covering all the data types that can be contained inside your
+[T1 + T2 + ...], covering all the data types that can be contained inside your
 type.
 - Each non-recursive constructor to a [GenLeaf]. Different constructors must use
   different variants of [T] to ensure they remain distinguishable!
 - Each recursive constructor to a [GenNode] where the [nat] is a (typically
   small) constant representing the constructor itself, and then all the data in
-  the constructor (recursive or otherwise) is put into child nodes. *)
+  the constructor (recursive or otherwise) is put into child nodes.
+
+This data type is the same as `GenTree.tree` in mathcomp, see
+https://github.com/math-comp/math-comp/blob/master/ssreflect/choice.v *)
 Inductive gen_tree (T : Type) : Type :=
   | GenLeaf : T → gen_tree T
   | GenNode : nat → list (gen_tree T) → gen_tree T.
-- 
GitLab