From 52baecf89ae62484fa05bf98bf9daa4259775e7e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 12 Jun 2019 18:49:09 +0200
Subject: [PATCH] Coqdoc tweaks.

---
 theories/proofmode/classes.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 3d5e6dc67..5b947614b 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -583,11 +583,11 @@ Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
 Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
 Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
 
-(* We make sure that tactics that perform actions on *specific* hypotheses or
+(** We make sure that tactics that perform actions on *specific* hypotheses or
 parts of the goal look through the [tc_opaque] connective, which is used to make
-definitions opaque for type class search. For example, when using `iDestruct`,
+definitions opaque for type class search. For example, when using [iDestruct],
 an explicit hypothesis is affected, and as such, we should look through opaque
-definitions. However, when using `iFrame` or `iNext`, arbitrary hypotheses or
+definitions. However, when using [iFrame] or [iNext], arbitrary hypotheses or
 parts of the goal are affected, and as such, type class opacity should be
 respected.
 
-- 
GitLab