work around Coq bug 5401 breaking 'Print HintDb typeclass_instances'

4172cacd · Ralf Jung · 4a154f08 · 4172cacd
Commit 4172cacd authored Mar 21, 2017 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 2 deletions

theories/algebra/vector.v theories/algebra/vector.v +2 -2

No files found.
--- 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 :