From 07ba4fef4583872456838cd1895fcb40798a0c2d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 9 Dec 2019 22:46:23 +0100
Subject: [PATCH] Coqdoc tweak.

---
 theories/proofmode/classes.v | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 2b678ed3c..a294222f0 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -134,17 +134,14 @@ Arguments IntoAbsorbingly {_} _%I _%I.
 Arguments into_absorbingly {_} _%I _%I {_}.
 Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
 
-(*
-Converting an assumption [R] into a wand [P -∗ Q] is done in three stages:
+(** Converting an assumption [R] into a wand [P -∗ Q] is done in three stages:
 
 - Strip modalities and universal quantifiers of [R] until an arrow or a wand
   has been obtained.
 - Balance modalities in the arguments [P] and [Q] to match the goal (which used
   for [iApply]) or the premise (when used with [iSpecialize] and a specific
   hypothesis).
-- Instantiate the premise of the wand or implication.
-*)
-
+- Instantiate the premise of the wand or implication. *)
 Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
   into_wand : □?p R ⊢ □?q P -∗ Q.
 Arguments IntoWand {_} _ _ _%I _%I _%I : simpl never.
-- 
GitLab