From 4172cacd403196d398e37b2bbb0fa0bba8540a1a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 21 Mar 2017 18:55:52 +0100
Subject: [PATCH] work around Coq bug 5401 breaking 'Print HintDb
 typeclass_instances'

---
 theories/algebra/vector.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/vector.v b/theories/algebra/vector.v
index 0cd7e7461..5f1b29130 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -40,10 +40,10 @@ Section proper.
   Context {A : ofeT}.
 
   Global Instance vcons_ne n :
-    Proper (dist n ==> forall_relation (λ _, dist n ==> dist n)) (@vcons A).
+    Proper (dist n ==> forall_relation (λ x, dist n ==> dist n)) (@vcons A).
   Proof. by constructor. Qed.
   Global Instance vcons_proper :
-    Proper (equiv ==> forall_relation (λ _, equiv ==> equiv)) (@vcons A).
+    Proper (equiv ==> forall_relation (λ x, equiv ==> equiv)) (@vcons A).
   Proof. by constructor. Qed.
 
   Global Instance vlookup_ne n m :
-- 
GitLab