From 676a5302a2fcb505575a6dea84d60d3426bc08c7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Tue, 21 Jan 2020 11:01:36 -0600
Subject: [PATCH] Fix typo spot by @Blaisorblade.
---
theories/algebra/big_op.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index 7bf52ebc..30b192b9 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -278,7 +278,7 @@ Section gmap.
(∀ k x, m !! k = Some x → f k x ≡ g k x) →
([^o map] k ↦ x ∈ m, f k x) ≡ ([^o map] k ↦ x ∈ m, g k x).
Proof. apply big_opM_gen_proper; apply _. Qed.
- (** The version [big_opL_proper_2] with [≡] for the map arguments can only be
+ (** The version [big_opM_proper_2] with [≡] for the map arguments can only be
used if there is a setoid on [A]. The version for [dist n] can be found in
[algebra.gmap]. We do not define this lemma as a [Proper] instance, since
[f_equiv] will then use sometimes use this one, and other times
--
GitLab