From 0dbb3948f4f1d385dc31ec9653d5fb5f7abd122d Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 18 Feb 2025 09:45:03 +0100 Subject: [PATCH] More CoqDoc. --- stdpp/countable.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/stdpp/countable.v b/stdpp/countable.v index 73993ceb..f6baeb4e 100644 --- a/stdpp/countable.v +++ b/stdpp/countable.v @@ -323,7 +323,7 @@ type. small) constant representing the constructor itself, and then all the data in the constructor (recursive or otherwise) is put into child nodes. -This data type is the same as `GenTree.tree` in mathcomp, see +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 -- GitLab