From b4f44c90f86ca59afecd67ef929ec6a83eb253d3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 31 May 2021 08:11:43 +0200
Subject: [PATCH] Coqdoc.

---
 theories/countable.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/countable.v b/theories/countable.v
index 5573876a..d73d18c9 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -3,7 +3,7 @@ From stdpp Require Export list numbers list_numbers fin.
 From stdpp Require Import options.
 Local Open Scope positive.
 
-(* Note that [Countable A] gives rise to [EqDecision A] by checking equality of
+(** Note that [Countable A] gives rise to [EqDecision A] by checking equality of
 the results of [encode]. This instance of [EqDecision A] is very inefficient, so
 the native decider is typically preferred for actual computation. To avoid
 overlapping instances, we include [EqDecision A] explicitly as a parameter of
-- 
GitLab