Improve linebreaks and coqdoc in comment.

iris/algebra/lib/gset_bij.v

@@ -2,15 +2,15 @@
 
 This RA is a view where the authoritative element is a partial bijection between
 types [A] and [B] and the fragments are subrels of the bijection. The data for
-the bijection is represented as a set of pairs [A*B], and the view relation
+the bijection is represented as a set of pairs [A * B], and the view relation
 enforces when an authoritative element is valid it is a bijection (that is, it
 is deterministic as a function from [A → option B] and [B → option A]).
 
 The fragments compose by set union, which means that fragments are their own
 core, ownership of a fragment is persistent, and the authoritative element can
-only grow (in that it can only map more pairs (a,b)). *)
+only grow (in that it can only map more pairs [(a,b)]). *)
 
-(** view needs to be exported for the canonical instances *)
+(* [algebra.view] needs to be exported for the canonical instances *)
 From iris.algebra Require Export view gset.
 From iris.algebra Require Import updates.
 From iris.prelude Require Import options.
@@ -19,7 +19,7 @@ Section gset_bijective.
   Context `{Countable A, Countable B}.
   Implicit Types (a : A) (b : B).
 
-  (** [gset_bijective] states that for a graph [L] of (a, b) pairs, [L] maps
+  (** [gset_bijective] states that for a graph [L] of [(a, b)] pairs, [L] maps
   from [A] to [B] and back deterministically. The key property characterizing
   [gset_bijective] is [gset_bijective_eq_iff]. *)
   Definition gset_bijective (L : gset (A * B)) :=

iris/base_logic/lib/gset_bij.v

 (** Propositions for reasoning about monotone partial bijections.
 
-This library provides two propositions [gset_bij_own_auth γ L] and [gset_bij_own_elem γ a b], where [L]
-is a bijection between types [A] and [B] represented by a set of associations
-[gset (A*B)]. The idea is that [gset_bij_own_auth γ L] is an authoritative bijection [L]
-while [gset_bij_own_elem γ a b] is a persistent resource saying [L] associates a and b.
+This library provides two propositions [gset_bij_own_auth γ L] and
+[gset_bij_own_elem γ a b], where [L] is a bijection between types [A] and [B]
+represented by a set of associations [gset (A * B)]. The idea is that
+[gset_bij_own_auth γ L] is an authoritative bijection [L], while
+[gset_bij_own_elem γ a b] is a persistent resource saying [L] associates [a]
+and [b].
 
 The main use case is in a logical relation-based proof where [L] maintains the
 association between locations [A] in one execution and [B] in another (perhaps
 of different types, if the logical relation relates two different semantics).
 
 The association [L] is always bijective, so that if [a] is mapped to [b], there
-should be no other mappings for either [a] or [b]; the [gset_bij_own_extend] update
-theorem enforces that new mappings respect this property, and [gset_bij_own_elem_agree]
-allows the user to exploit bijectivity. The bijection grows monotonically, so
-that the set of associations only grows; this is captured by the persistence of
-[gset_bij_own_elem].
+should be no other mappings for either [a] or [b]; the [gset_bij_own_extend]
+update theorem enforces that new mappings respect this property, and
+[gset_bij_own_elem_agree] allows the user to exploit bijectivity. The bijection
+grows monotonically, so that the set of associations only grows; this is
+captured by the persistence of [gset_bij_own_elem].
 
-This library is a logical, ownership-based wrapper around gset_bij. *)
+This library is a logical, ownership-based wrapper around [gset_bij]. *)
 
 From iris.algebra.lib Require Import gset_bij.
 From iris.bi.lib Require Import fractional.