From e383889e3a8edd80133b37dc8966a2c80762f4e3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Mar 2017 12:24:36 +0100
Subject: [PATCH] Remove Hint Mode that was already declared elsewhere (in
classes.v).
---
theories/proofmode/class_instances.v | 2 --
1 file changed, 2 deletions(-)
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 44c6d36a6..e2f04a721 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -707,5 +707,3 @@ Proof.
by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
Qed.
End classes.
-
-Hint Mode IntoLaterN' + - ! - : typeclass_instances.
--
GitLab