From 56e1bfd72e4b094e1381168ce61bbf1f68c9d150 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 3 May 2018 22:04:02 +0200
Subject: [PATCH] Fix `Hint Mode` of `IntoAbsorbingly`.

---
 theories/proofmode/classes.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index cf32bcd96..f892b7bff 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -124,11 +124,14 @@ Arguments from_affinely {_} _%I _%I {_}.
 Hint Mode FromAffinely + ! - : typeclass_instances.
 Hint Mode FromAffinely + - ! : typeclass_instances.
 
+(** The [IntoAbsorbingly P Q] class is used to add an [<absorb>] modality to
+the proposition [Q].
+
+The input is [Q] and the output is [P]. *)
 Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
   into_absorbingly : P ⊢ <absorb> Q.
 Arguments IntoAbsorbingly {_} _%I _%I.
 Arguments into_absorbingly {_} _%I _%I {_}.
-Hint Mode IntoAbsorbingly + ! -  : typeclass_instances.
 Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
 
 (*
-- 
GitLab