Commit 676a5302 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix typo spot by @Blaisorblade.

parent 4a45cda0
......@@ -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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment