From 5c61abfb097be9139280d01675ea89496353672e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Sat, 8 Dec 2018 17:14:21 +0100
Subject: [PATCH] Close issue #223: make instance anonymous and put a comment
why the instance is there.
---
theories/algebra/big_op.v | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index 9f04dd7e..8d9110ef 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -413,7 +413,11 @@ Section homomorphisms.
Context `{Monoid M1 o1, Monoid M2 o2}.
Infix "`o1`" := o1 (at level 50, left associativity).
Infix "`o2`" := o2 (at level 50, left associativity).
- Instance foo {A} (R : relation A) : RewriteRelation R.
+ (** The ssreflect rewrite tactic only works for relations that have a
+ [RewriteRelation] instance. For the purpose of this section, we want to
+ rewrite with arbitrary relations, so we declare any relation to be a
+ [RewriteRelation]. *)
+ Local Instance: ∀ {A} (R : relation A), RewriteRelation R.
Lemma big_opL_commute {A} (h : M1 → M2) `{!MonoidHomomorphism o1 o2 R h}
(f : nat → A → M1) l :
--
GitLab