multi line comments don't have a title

3 files changed, 96 insertions, 56 deletions

diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index 315c2fdaeb..cf4b8c1ce9 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -13,8 +13,8 @@
 Require Bool.
 Require Import ssreflect ssrfun.
 
-
-(**  A theory of boolean predicates and operators. A large part of this file is
+(**
+ A theory of boolean predicates and operators. A large part of this file is
  concerned with boolean reflection.
  Definitions and notations:
                is_true b == the coercion of b : bool to Prop (:= b = true).
@@ -288,7 +288,8 @@ Reserved Notation "x \notin A"
 Reserved Notation "p1 =i p2"
   (at level 70, format "'[hv' p1 '/ '  =i  p2 ']'", no associativity).
 
-(**  We introduce a number of n-ary "list-style" notations that share a common
+(**
+ We introduce a number of n-ary "list-style" notations that share a common
  format, namely
     #[#op arg1, arg2, ... last_separator last_arg#]#
  This usually denotes a right-associative applications of op, e.g.,
@@ -348,7 +349,7 @@ Reserved Notation "[ 'rel' x y : T => E ]" (at level 0, x, y at level 8, format
 Delimit Scope bool_scope with B.
 Open Scope bool_scope.
 
-(**  An alternative to xorb that behaves somewhat better wrt simplification.     **)
+(**  An alternative to xorb that behaves somewhat better wrt simplification. **)
 Definition addb b := if b then negb else id.
 
 (**  Notation for && and || is declared in Init.Datatypes.  **)
@@ -376,7 +377,8 @@ Definition notF := not_false_is_true.
 
 (**  Negation lemmas.  **)
 
-(**  We generally take NEGATION as the standard form of a false condition:
+(**
+ We generally take NEGATION as the standard form of a false condition:
  negative boolean hypotheses should be of the form ~~ b, rather than ~ b or
  b = false, as much as possible.                                             **)
 
@@ -426,7 +428,8 @@ Proof. by move/contra=> notb_notc /notb_notc/negbTE. Qed.
 Lemma contraFF (c b : bool) : (c -> b) -> b = false -> c = false.
 Proof. by move/contraFN=> bF_notc /bF_notc/negbTE. Qed.
 
-(**  Coercion of sum-style datatypes into bool, which makes it possible
+(**
+ Coercion of sum-style datatypes into bool, which makes it possible
  to use ssr's boolean if rather than Coq's "generic" if.             **)
 
 Coercion isSome T (u : option T) := if u is Some _ then true else false.
@@ -441,7 +444,8 @@ Prenex Implicits  isSome is_inl is_left is_inleft.
 
 Definition decidable P := {P} + {~ P}.
 
-(**  Lemmas for ifs with large conditions, which allow reasoning about the
+(**
+ Lemmas for ifs with large conditions, which allow reasoning about the
  condition without repeating it inside the proof (the latter IS
  preferable when the condition is short).
  Usage :
@@ -483,7 +487,7 @@ Lemma if_arg (fT fF : A -> B) :
   (if b then fT else fF) x = if b then fT x else fF x.
 Proof. by case b. Qed.
 
-(**  Turning a boolean "if" form into an application.                            **)
+(**  Turning a boolean "if" form into an application.  **)
 Definition if_expr := if b then vT else vF.
 Lemma ifE : (if b then vT else vF) = if_expr. Proof. by []. Qed.
 
@@ -584,7 +588,7 @@ Lemma rwP : P <-> b. Proof. by split; [apply: introT | apply: elimT]. Qed.
 Lemma rwP2 : reflect Q b -> (P <-> Q).
 Proof. by move=> Qb; split=> ?; [apply: appP | apply: elimT; case: Qb]. Qed.
 
-(**   Predicate family to reflect excluded middle in bool.                       **)
+(**   Predicate family to reflect excluded middle in bool.  **)
 Variant alt_spec : bool -> Type :=
   | AltTrue of     P : alt_spec true
   | AltFalse of ~~ b : alt_spec false.
@@ -637,7 +641,8 @@ Proof. by split; apply=> [hC|hP]; [apply/unlessL/unlessL | apply/unlessR]. Qed.
 Lemma unless_contra b C : implies (~~ b -> C) (\unless C, b).
 Proof. by split; case: b => [_ | hC]; [apply/unlessR | apply/unlessL/hC]. Qed.
 
-(**  Classical reasoning becomes directly accessible for any bool subgoal.
+(**
+ Classical reasoning becomes directly accessible for any bool subgoal.
  Note that we cannot use "unless" here for lack of universe polymorphism.    **)
 Definition classically P : Prop := forall b : bool, (P -> b) -> b.
 
@@ -669,7 +674,8 @@ move=> iPQ []// notPQ; apply/notPQ=> /iPQ-cQ.
 by case: notF; apply: cQ => hQ; apply: notPQ.
 Qed.
 
-(**  List notations for wider connectives; the Prop connectives have a fixed
+(**
+ List notations for wider connectives; the Prop connectives have a fixed
  width so as to avoid iterated destruction (we go up to width 5 for /\, and
  width 4 for or). The bool connectives have arbitrary widths, but denote
  expressions that associate to the RIGHT. This is consistent with the right
@@ -946,7 +952,8 @@ Lemma addbP a b : reflect (~~ a = b) (a (+) b).
 Proof. by case: a; case: b; constructor. Qed.
 Arguments addbP [a b].
 
-(**  Resolution tactic for blindly weeding out common terms from boolean
+(**
+ Resolution tactic for blindly weeding out common terms from boolean
  equalities. When faced with a goal of the form (andb/orb/addb b1 b2) = b3
  they will try to locate b1 in b3 and remove it. This can fail!             **)
 
@@ -964,7 +971,8 @@ Ltac bool_congr :=
   end.
 
 
-(**  Predicates, i.e., packaged functions to bool.
+(**
+ Predicates, i.e., packaged functions to bool.
  - pred T, the basic type for predicates over a type T, is simply an alias
  for T -> bool.
  We actually distinguish two kinds of predicates, which we call applicative
@@ -1094,7 +1102,8 @@ Coercion applicative_pred_of_simpl (p : simpl_pred) : applicative_pred :=
   fun_of_simpl p.
 Coercion collective_pred_of_simpl (p : simpl_pred) : collective_pred :=
   fun x => (let: SimplFun f := p in fun _ => f x) x.
-(**  Note: applicative_of_simpl is convertible to pred_of_simpl, while
+(**
+ Note: applicative_of_simpl is convertible to pred_of_simpl, while
  collective_of_simpl is not.  **)
 
 Definition pred0 := SimplPred xpred0.
@@ -1166,7 +1175,8 @@ Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T => E%B))
 Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ _ id)
   (at level 0, format "[ 'predType'  'of'  T ]") : form_scope.
 
-(**  This redundant coercion lets us "inherit" the simpl_predType canonical
+(**
+ This redundant coercion lets us "inherit" the simpl_predType canonical
  instance by declaring a coercion to simpl_pred. This hack is the only way
  to put a predType structure on a predArgType. We use simpl_pred rather
  than pred to ensure that /= removes the identity coercion. Note that the
@@ -1176,7 +1186,8 @@ Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ _ id)
 Notation pred_class := (pred_sort (predPredType _)).
 Coercion sort_of_simpl_pred T (p : simpl_pred T) : pred_class := p : pred T.
 
-(**  This lets us use some types as a synonym for their universal predicate.
+(**
+ This lets us use some types as a synonym for their universal predicate.
  Unfortunately, this won't work for existing types like bool, unless we
  redefine bool, true, false and all bool ops.                                **)
 Definition predArgType := Type.
@@ -1187,7 +1198,8 @@ Coercion pred_of_argType (T : predArgType) : simpl_pred T := predT.
 Notation "{ : T }" := (T%type : predArgType)
   (at level 0, format "{ :  T }") : type_scope.
 
-(**  These must be defined outside a Section because "cooking" kills the
+(**
+ These must be defined outside a Section because "cooking" kills the
  nosimpl tag.                                                                **)
 
 Definition mem T (pT : predType T) : pT -> mem_pred T :=
@@ -1254,7 +1266,8 @@ Section simpl_mem.
 Variables (T : Type) (pT : predType T).
 Implicit Types (x : T) (p : pred T) (sp : simpl_pred T) (pp : pT).
 
-(**  Bespoke structures that provide fine-grained control over matching the
+(**
+ Bespoke structures that provide fine-grained control over matching the
  various forms of the \in predicate; note in particular the different forms
  of hoisting that are used. We had to work around several bugs in the
  implementation of unification, notably improper expansion of telescope
@@ -1305,7 +1318,8 @@ Lemma in_simpl x p (msp : manifest_simpl_pred p) :
   in_mem x (Mem [eta fun_of_simpl (msp : simpl_pred T)]) = p x.
 Proof. by case: msp => _ /= ->. Qed.
 
-(**  Because of the explicit eta expansion in the left-hand side, this lemma
+(**
+ Because of the explicit eta expansion in the left-hand side, this lemma
  should only be used in a right-to-left direction. The 8.3 hack allowing
  partial right-to-left use does not work with the improved expansion
  heuristics in 8.4.                                                          **)
@@ -1388,7 +1402,8 @@ Definition KeyedPred := @PackKeyedPred k p (frefl _).
 Variable k_p : keyed_pred k.
 Lemma keyed_predE : k_p =i p. Proof. by case: k_p. Qed.
 
-(**  Instances that strip the mem cast; the first one has "pred_of_mem" as its
+(**
+ Instances that strip the mem cast; the first one has "pred_of_mem" as its
  projection head value, while the second has "pred_of_simpl". The latter
  has the side benefit of preempting accidental misdeclarations.
  Note: pred_of_mem is the registered mem >-> pred_class coercion, while
@@ -1461,7 +1476,8 @@ Proof. by move=> y0; apply: all_sig_cond_dep. Qed.
 
 Section RelationProperties.
 
-(**  Caveat: reflexive should not be used to state lemmas, as auto and trivial
+(**
+ Caveat: reflexive should not be used to state lemmas, as auto and trivial
  will not expand the constant.                                               **)
 
 Variable T : Type.
@@ -1496,7 +1512,8 @@ Proof. by move=> x y /sym_left_transitive Rxy z; rewrite !(symR z) Rxy. Qed.
 
 End PER.
 
-(**  We define the equivalence property with prenex quantification so that it
+(**
+ We define the equivalence property with prenex quantification so that it
  can be localized using the {in ..., ..} form defined below.                 **)
 
 Definition equivalence_rel := forall x y z, R z z * (R x y -> R x z = R y z).
@@ -1626,7 +1643,8 @@ Notation "{ 'on' cd , 'bijective' f }" := (bijective_on (mem cd) f)
   (at level 0, f at level 8,
    format "{ 'on'  cd ,  'bijective'  f }") : type_scope.
 
-(**  Weakening and monotonicity lemmas for localized predicates.
+(**
+ Weakening and monotonicity lemmas for localized predicates.
  Note that using these lemmas in backward reasoning will force expansion of
  the predicate definition, as Coq needs to expose the quantifier to apply
  these lemmas. We define a few specialized variants to avoid this for some
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 3bd86063d7..80e9cc8489 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -15,7 +15,8 @@ Require Import ssrmatching.
 Declare ML Module "ssreflect_plugin".
 
 
-(**  This file is the Gallina part of the ssreflect plugin implementation.
+(**
+ This file is the Gallina part of the ssreflect plugin implementation.
  Files that use the ssreflect plugin should always Require ssreflect and
  either Import ssreflect or Import ssreflect.SsrSyntax.
    Part of the contents of this file is technical and will only interest
@@ -62,7 +63,8 @@ Unset Printing Implicit Defensive.
 
 Module SsrSyntax.
 
-(**  Declare Ssr keywords: 'is' 'of' '//' '/=' and '//='. We also declare the
+(**
+ Declare Ssr keywords: 'is' 'of' '//' '/=' and '//='. We also declare the
  parsing level 8, as a workaround for a notation grammar factoring problem.
  Arguments of application-style notations (at level 10) should be declared
  at level 8 rather than 9 or the camlp5 grammar will not factor properly.    **)
@@ -81,7 +83,8 @@ End SsrSyntax.
 Export SsrMatchingSyntax.
 Export SsrSyntax.
 
-(**  Make the general "if" into a notation, so that we can override it below.
+(**
+ Make the general "if" into a notation, so that we can override it below.
  The notations are "only parsing" because the Coq decompiler will not
  recognize the expansion of the boolean if; using the default printer
  avoids a spurrious trailing %%GEN_IF.                                        **)
@@ -102,7 +105,7 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" :=
   (at level 200, c, t, v1, v2 at level 200, x ident, only parsing)
      : general_if_scope.
 
-(**  Force boolean interpretation of simple if expressions.                      **)
+(**  Force boolean interpretation of simple if expressions.  **)
 
 Declare Scope boolean_if_scope.
 Delimit Scope boolean_if_scope with BOOL_IF.
@@ -118,7 +121,8 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" :=
 
 Open Scope boolean_if_scope.
 
-(**  To allow a wider variety of notations without reserving a large number of
+(**
+ To allow a wider variety of notations without reserving a large number of
  of identifiers, the ssreflect library systematically uses "forms" to
  enclose complex mixfix syntax. A "form" is simply a mixfix expression
  enclosed in square brackets and introduced by a keyword:
@@ -131,7 +135,8 @@ Declare Scope form_scope.
 Delimit Scope form_scope with FORM.
 Open Scope form_scope.
 
-(**  Allow overloading of the cast (x : T) syntax, put whitespace around the
+(**
+ Allow overloading of the cast (x : T) syntax, put whitespace around the
  ":" symbol to avoid lexical clashes (and for consistency with the parsing
  precedence of the notation, which binds less tightly than application),
  and put printing boxes that print the type of a long definition on a
@@ -140,12 +145,13 @@ Notation "x : T" := (x : T)
   (at level 100, right associativity,
    format "'[hv' x '/ '  :  T ']'") : core_scope.
 
-(**  Allow the casual use of notations like nat * nat for explicit Type
+(**
+ Allow the casual use of notations like nat * nat for explicit Type
  declarations. Note that (nat * nat : Type) is NOT equivalent to
- (nat * nat)%%type, whose inferred type is legacy type "Set".                 **)
+ (nat * nat)%%type, whose inferred type is legacy type "Set".                **)
 Notation "T : 'Type'" := (T%type : Type)
   (at level 100, only parsing) : core_scope.
-(**  Allow similarly Prop annotation for, e.g., rewrite multirules.              **)
+(**  Allow similarly Prop annotation for, e.g., rewrite multirules. **)
 Notation "P : 'Prop'" := (P%type : Prop)
   (at level 100, only parsing) : core_scope.
 
@@ -166,7 +172,8 @@ Register abstract as plugins.ssreflect.abstract.
 (**  Constants for tactic-views  **)
 Inductive external_view : Type := tactic_view of Type.
 
-(**  Syntax for referring to canonical structures:
+(**
+ Syntax for referring to canonical structures:
       #[#the struct_type of proj_val by proj_fun#]#
  This form denotes the Canonical instance s of the Structure type
  struct_type whose proj_fun projection is proj_val, i.e., such that
@@ -210,7 +217,8 @@ Notation "[ 'the' sT 'of' v 'by' f ]" :=
 Notation "[ 'the' sT 'of' v ]" := (get ((fun s : sT => Put v (*coerce*)s s) _))
   (at level 0, only parsing) : form_scope.
 
-(**  The following are "format only" versions of the above notations. Since Coq
+(**
+ The following are "format only" versions of the above notations. Since Coq
  doesn't provide this facility, we fake it by splitting the "the" keyword.
  We need to do this to prevent the formatter from being be thrown off by
  application collapsing, coercion insertion and beta reduction in the right
@@ -222,12 +230,14 @@ Notation "[ 'th' 'e' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _)
 Notation "[ 'th' 'e' sT 'of' v ]" := (@get _ sT v _ _)
   (at level 0, format "[ 'th' 'e'  sT  'of'  v ]") : form_scope.
 
-(**  We would like to recognize
+(**
+ We would like to recognize
 Notation " #[# 'th' 'e' sT 'of' v : 'Type' #]#" := (@get Type sT v _ _)
   (at level 0, format " #[# 'th' 'e'  sT   'of'  v  :  'Type' #]#") : form_scope.
  **)
 
-(**  Helper notation for canonical structure inheritance support.
+(**
+ Helper notation for canonical structure inheritance support.
  This is a workaround for the poor interaction between delta reduction and
  canonical projections in Coq's unification algorithm, by which transparent
  definitions hide canonical instances, i.e., in
@@ -261,7 +271,8 @@ Definition returnType aT rT & aT -> rT := rT.
 Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s)
   (at level 0, format "{ 'type'  'of'  c  'for'  s }") : type_scope.
 
-(**  A generic "phantom" type (actually, a unit type with a phantom parameter).
+(**
+ A generic "phantom" type (actually, a unit type with a phantom parameter).
  This type can be used for type definitions that require some Structure
  on one of their parameters, to allow Coq to infer said structure so it
  does not have to be supplied explicitly or via the " #[#the _ of _ #]#" notation
@@ -287,13 +298,14 @@ Arguments phantom : clear implicits.
 Arguments Phantom : clear implicits.
 Variant phant (p : Type) := Phant.
 
-(**  Internal tagging used by the implementation of the ssreflect elim.          **)
+(**  Internal tagging used by the implementation of the ssreflect elim.  **)
 
 Definition protect_term (A : Type) (x : A) : A := x.
 
 Register protect_term as plugins.ssreflect.protect_term.
 
-(**  The ssreflect idiom for a non-keyed pattern:
+(**
+ The ssreflect idiom for a non-keyed pattern:
   - unkeyed t wiil match any subterm that unifies with t, regardless of
     whether it displays the same head symbol as t.
   - unkeyed t a b will match any application of a term f unifying with t,
@@ -308,7 +320,8 @@ Notation unkeyed x := (let flex := x in flex).
 Definition ssr_converse R (r : R) := (Logic.I, r).
 Notation "=^~ r" := (ssr_converse r) (at level 100) : form_scope.
 
-(**  Term tagging (user-level).
+(**
+ Term tagging (user-level).
  The ssreflect library uses four strengths of term tagging to restrict
  convertibility during type checking:
   nosimpl t simplifies to t EXCEPT in a definition; more precisely, given
@@ -347,11 +360,11 @@ Register locked as plugins.ssreflect.locked.
 
 Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed.
 
-(**  Needed for locked predicates, in particular for eqType's.                   **)
+(**  Needed for locked predicates, in particular for eqType's.  **)
 Lemma not_locked_false_eq_true : locked false <> true.
 Proof. unlock; discriminate. Qed.
 
-(**  The basic closing tactic "done".                                            **)
+(**  The basic closing tactic "done".  **)
 Ltac done :=
   trivial; hnf; intros; solve
    [ do ![solve [trivial | apply: sym_equal; trivial]
@@ -382,7 +395,8 @@ Notation "[ 'unlockable' 'fun' C ]" := (@Unlockable _ (fun _ => _) C (unlock _))
 (**  The argument order ensures that k is always compared before T.  **)
 Definition locked_with k := let: tt := k in fun T x => x : T.
 
-(**  This can be used as a cheap alternative to cloning the unlockable instance
+(**
+ This can be used as a cheap alternative to cloning the unlockable instance
  below, but with caution as unkeyed matching can be expensive.               **)
 Lemma locked_withE T k x : unkeyed (locked_with k x) = x :> T.
 Proof. by case: k. Qed.
@@ -395,7 +409,7 @@ Canonical locked_with_unlockable T k x :=
 Lemma unlock_with T k x : unlocked (locked_with_unlockable k x) = x :> T.
 Proof. exact: unlock. Qed.
 
-(**  The internal lemmas for the have tactics.                                   **)
+(**  The internal lemmas for the have tactics.  **)
 
 Definition ssr_have Plemma Pgoal (step : Plemma) rest : Pgoal := rest step.
 Arguments ssr_have Plemma [Pgoal].
@@ -416,7 +430,7 @@ Arguments ssr_wlog Plemma [Pgoal].
 Register ssr_suff as plugins.ssreflect.ssr_suff.
 Register ssr_wlog as plugins.ssreflect.ssr_wlog.
 
-(**  Internal N-ary congruence lemmas for the congr tactic.                      **)
+(**  Internal N-ary congruence lemmas for the congr tactic.  **)
 
 Fixpoint nary_congruence_statement (n : nat)
          : (forall B, (B -> B -> Prop) -> Prop) -> Prop :=
@@ -443,7 +457,7 @@ Arguments ssr_congr_arrow : clear implicits.
 Register nary_congruence as plugins.ssreflect.nary_congruence.
 Register ssr_congr_arrow as plugins.ssreflect.ssr_congr_arrow.
 
-(**  View lemmas that don't use reflection.                                      **)
+(**  View lemmas that don't use reflection.  **)
 
 Section ApplyIff.
 
@@ -461,7 +475,8 @@ End ApplyIff.
 Hint View for move/ iffLRn|2 iffRLn|2 iffLR|2 iffRL|2.
 Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2.
 
-(**  To focus non-ssreflect tactics on a subterm, eg vm_compute.
+(**
+ To focus non-ssreflect tactics on a subterm, eg vm_compute.
  Usage:
    elim/abstract_context: (pattern) => G defG.
    vm_compute; rewrite {}defG {G}.
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index 70be97feec..4d458ee765 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -13,7 +13,8 @@
 Require Import ssreflect.
 
 
-(**  This file contains the basic definitions and notations for working with
+(**
+ This file contains the basic definitions and notations for working with
  functions. The definitions provide for:
 
  - Pair projections:
@@ -241,7 +242,8 @@ Coercion pair_of_and P Q (PandQ : P /\ Q) := (proj1 PandQ, proj2 PandQ).
 Definition all_pair I T U (w : forall i : I, T i * U i) :=
   (fun i => (w i).1, fun i => (w i).2).
 
-(**  Complements on the option type constructor, used below to
+(**
+ Complements on the option type constructor, used below to
  encode partial functions.                                   **)
 
 Module Option.
@@ -274,7 +276,7 @@ Definition congr2 := f_equal2.
 (**  Force at least one implicit when used as a view.  **)
 Prenex Implicits esym nesym.
 
-(**  A predicate for singleton types.                                            **)
+(**  A predicate for singleton types.  **)
 Definition all_equal_to T (x0 : T) := forall x, unkeyed x = x0.
 
 Lemma unitE : all_equal_to tt. Proof. by case. Qed.
@@ -286,7 +288,8 @@ Canonical wrap T x := @Wrap T x.
 
 Prenex Implicits unwrap wrap Wrap.
 
-(**  Syntax for defining auxiliary recursive function.
+(**
+ Syntax for defining auxiliary recursive function.
   Usage:
  Section FooDefinition.
  Variables (g1 : T1) (g2 : T2).  (globals)
@@ -321,7 +324,8 @@ Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]"
   (at level 0,
   format "[ 'rec'  a0 ,  a1 ,  a2 ,  a3 ,  a4 ,  a5 ,  a6 ,  a7 ,  a8 ,  a9 ]").
 
-(**  Definitions and notation for explicit functions with simplification,
+(**
+ Definitions and notation for explicit functions with simplification,
  i.e., which simpl and /= beta expand (this is complementary to nosimpl).  **)
 
 Section SimplFun.
@@ -367,7 +371,8 @@ Notation "[ 'fun' ( x : xT ) ( y : yT ) => E ]" :=
 (**  For delta functions in eqtype.v.  **)
 Definition SimplFunDelta aT rT (f : aT -> aT -> rT) := [fun z => f z z].
 
-(**  Extensional equality, for unary and binary functions, including syntactic
+(**
+ Extensional equality, for unary and binary functions, including syntactic
  sugar.                                                                      **)
 
 Section ExtensionalEquality.
@@ -602,7 +607,8 @@ Notation "{ 'mono' f : x y /~ a }" :=
   (at level 0, f at level 99, x ident, y ident,
    format "{ 'mono'  f  :  x  y  /~  a }") : type_scope.
 
-(**  In an intuitionistic setting, we have two degrees of injectivity. The
+(**
+ In an intuitionistic setting, we have two degrees of injectivity. The
  weaker one gives only simplification, and the strong one provides a left
  inverse (we show in `fintype' that they coincide for finite types).
  We also define an intermediate version where the left inverse is only a
@@ -610,7 +616,8 @@ Notation "{ 'mono' f : x y /~ a }" :=
 
 Section Injections.
 
-(**  rT must come first so we can use @ to mitigate the Coq 1st order
+(**
+ rT must come first so we can use @ to mitigate the Coq 1st order
  unification bug (e..g., Coq can't infer rT from a "cancel" lemma).  **)
 Variables (rT aT : Type) (f : aT -> rT).
 
@@ -644,7 +651,7 @@ Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed.
 (**  Force implicits to use as a view.  **)
 Prenex Implicits Some_inj.
 
-(**  cancellation lemmas for dependent type casts.                              **)
+(**  cancellation lemmas for dependent type casts. **)
 Lemma esymK T x y : cancel (@esym T x y) (@esym T y x).
 Proof. by case: y /. Qed.