[doc] adapt comments in plugins/ssr/*.v to coqdoc style

3 files changed, 896 insertions, 896 deletions

diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index 0865f75ec5..315c2fdaeb 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -13,261 +13,261 @@
 Require Bool.
 Require Import ssreflect ssrfun.
 
-(******************************************************************************)
-(* 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). *)
-(*                            This is just input and displayed as `b''.       *)
-(*             reflect P b == the reflection inductive predicate, asserting   *)
-(*                            that the logical proposition P : prop with the  *)
-(*                            formula b : bool. Lemmas asserting reflect P b  *)
-(*                            are often referred to as "views".               *)
-(*  iffP, appP, sameP, rwP :: lemmas for direct manipulation of reflection    *)
-(*                            views: iffP is used to prove reflection from    *)
-(*                            logical equivalence, appP to compose views, and *)
-(*                            sameP and rwP to perform boolean and setoid     *)
-(*                            rewriting.                                      *)
-(*                   elimT :: coercion reflect >-> Funclass, which allows the *)
-(*                            direct application of `reflect' views to        *)
-(*                            boolean assertions.                             *)
-(*             decidable P <-> P is effectively decidable (:= {P} + {~ P}.    *)
-(*    contra, contraL, ... :: contraposition lemmas.                          *)
-(*           altP my_viewP :: natural alternative for reflection; given       *)
-(*                            lemma myviewP: reflect my_Prop my_formula,      *)
-(*                              have [myP | not_myP] := altP my_viewP.        *)
-(*                            generates two subgoals, in which my_formula has *)
-(*                            been replaced by true and false, resp., with    *)
-(*                            new assumptions myP : my_Prop and               *)
-(*                            not_myP: ~~ my_formula.                         *)
-(*                            Caveat: my_formula must be an APPLICATION, not  *)
-(*                            a variable, constant, let-in, etc. (due to the  *)
-(*                            poor behaviour of dependent index matching).    *)
-(*        boolP my_formula :: boolean disjunction, equivalent to              *)
-(*                            altP (idP my_formula) but circumventing the     *)
-(*                            dependent index capture issue; destructing      *)
-(*                            boolP my_formula generates two subgoals with    *)
-(*                            assumtions my_formula and ~~ myformula. As      *)
-(*                            with altP, my_formula must be an application.   *)
-(*            \unless C, P <-> we can assume property P when a something that *)
-(*                            holds under condition C (such as C itself).     *)
-(*                         := forall G : Prop, (C -> G) -> (P -> G) -> G.     *)
-(*                            This is just C \/ P or rather its impredicative *)
-(*                            encoding, whose usage better fits the above     *)
-(*                            description: given a lemma UCP whose conclusion *)
-(*                            is \unless C, P we can assume P by writing:     *)
-(*                              wlog hP: / P by apply/UCP; (prove C -> goal). *)
-(*                           or even apply: UCP id _ => hP if the goal is C.  *)
-(*           classically P <-> we can assume P when proving is_true b.        *)
-(*                         := forall b : bool, (P -> b) -> b.                 *)
-(*                            This is equivalent to ~ (~ P) when P : Prop.    *)
-(*             implies P Q == wrapper variant type that coerces to P -> Q and *)
-(*                            can be used as a P -> Q view unambigously.      *)
-(*                            Useful to avoid spurious insertion of <-> views *)
-(*                            when Q is a conjunction of foralls, as in Lemma *)
-(*                            all_and2 below; conversely, avoids confusion in *)
-(*                            apply views for impredicative properties, such  *)
-(*                            as \unless C, P. Also supports contrapositives. *)
-(*                  a && b == the boolean conjunction of a and b.             *)
-(*                  a || b == the boolean disjunction of a and b.             *)
-(*                 a ==> b == the boolean implication of b by a.              *)
-(*                    ~~ a == the boolean negation of a.                      *)
-(*                 a (+) b == the boolean exclusive or (or sum) of a and b.   *)
-(*     [ /\ P1 , P2 & P3 ] == multiway logical conjunction, up to 5 terms.    *)
-(*     [ \/ P1 , P2 | P3 ] == multiway logical disjunction, up to 4 terms.    *)
-(*        [&& a, b, c & d] == iterated, right associative boolean conjunction *)
-(*                            with arbitrary arity.                           *)
-(*        [|| a, b, c | d] == iterated, right associative boolean disjunction *)
-(*                            with arbitrary arity.                           *)
-(*      [==> a, b, c => d] == iterated, right associative boolean implication *)
-(*                            with arbitrary arity.                           *)
-(*              and3P, ... == specific reflection lemmas for iterated         *)
-(*                            connectives.                                    *)
-(*       andTb, orbAC, ... == systematic names for boolean connective         *)
-(*                            properties (see suffix conventions below).      *)
-(*              prop_congr == a tactic to move a boolean equality from        *)
-(*                            its coerced form in Prop to the equality        *)
-(*                            in bool.                                        *)
-(*              bool_congr == resolution tactic for blindly weeding out       *)
-(*                            like terms from boolean equalities (can fail).  *)
-(* This file provides a theory of boolean predicates and relations:           *)
-(*                  pred T == the type of bool predicates (:= T -> bool).     *)
-(*            simpl_pred T == the type of simplifying bool predicates, using  *)
-(*                            the simpl_fun from ssrfun.v.                    *)
-(*                   rel T == the type of bool relations.                     *)
-(*                         := T -> pred T or T -> T -> bool.                  *)
-(*             simpl_rel T == type of simplifying relations.                  *)
-(*                predType == the generic predicate interface, supported for  *)
-(*                            for lists and sets.                             *)
-(*              pred_class == a coercion class for the predType projection to *)
-(*                            pred; declaring a coercion to pred_class is an  *)
-(*                            alternative way of equipping a type with a      *)
-(*                            predType structure, which interoperates better  *)
-(*                            with coercion subtyping. This is used, e.g.,    *)
-(*                            for finite sets, so that finite groups inherit  *)
-(*                            the membership operation by coercing to sets.   *)
-(* If P is a predicate the proposition "x satisfies P" can be written         *)
-(* applicatively as (P x), or using an explicit connective as (x \in P); in   *)
-(* the latter case we say that P is a "collective" predicate. We use A, B     *)
-(* rather than P, Q for collective predicates:                                *)
-(*                 x \in A == x satisfies the (collective) predicate A.       *)
-(*              x \notin A == x doesn't satisfy the (collective) predicate A. *)
-(* The pred T type can be used as a generic predicate type for either kind,   *)
-(* but the two kinds of predicates should not be confused. When a "generic"   *)
-(* pred T value of one type needs to be passed as the other the following     *)
-(* conversions should be used explicitly:                                     *)
-(*             SimplPred P == a (simplifying) applicative equivalent of P.    *)
-(*                   mem A == an applicative equivalent of A:                 *)
-(*                            mem A x simplifies to x \in A.                  *)
-(* Alternatively one can use the syntax for explicit simplifying predicates   *)
-(* and relations (in the following x is bound in E):                          *)
-(*            [pred x | E] == simplifying (see ssrfun) predicate x => E.      *)
-(*        [pred x : T | E] == predicate x => E, with a cast on the argument.  *)
-(*          [pred : T | P] == constant predicate P on type T.                 *)
-(*      [pred x | E1 & E2] == [pred x | E1 && E2]; an x : T cast is allowed.  *)
-(*           [pred x in A] == [pred x | x in A].                              *)
-(*       [pred x in A | E] == [pred x | x in A & E].                          *)
-(* [pred x in A | E1 & E2] == [pred x in A | E1 && E2].                       *)
-(*           [predU A & B] == union of two collective predicates A and B.     *)
-(*           [predI A & B] == intersection of collective predicates A and B.  *)
-(*           [predD A & B] == difference of collective predicates A and B.    *)
-(*               [predC A] == complement of the collective predicate A.       *)
-(*          [preim f of A] == preimage under f of the collective predicate A. *)
-(*          predU P Q, ... == union, etc of applicative predicates.           *)
-(*                   pred0 == the empty predicate.                            *)
-(*                   predT == the total (always true) predicate.              *)
-(*                            if T : predArgType, then T coerces to predT.    *)
-(*                   {: T} == T cast to predArgType (e.g., {: bool * nat})    *)
-(* In the following, x and y are bound in E:                                  *)
-(*           [rel x y | E] == simplifying relation x, y => E.                 *)
-(*       [rel x y : T | E] == simplifying relation with arguments cast.       *)
-(*  [rel x y in A & B | E] == [rel x y | [&& x \in A, y \in B & E]].          *)
-(*      [rel x y in A & B] == [rel x y | (x \in A) && (y \in B)].             *)
-(*      [rel x y in A | E] == [rel x y in A & A | E].                         *)
-(*          [rel x y in A] == [rel x y in A & A].                             *)
-(*                relU R S == union of relations R and S.                     *)
-(* Explicit values of type pred T (i.e., lamdba terms) should always be used  *)
-(* applicatively, while values of collection types implementing the predType  *)
-(* interface, such as sequences or sets should always be used as collective   *)
-(* predicates. Defined constants and functions of type pred T or simpl_pred T *)
-(* as well as the explicit simpl_pred T values described below, can generally *)
-(* be used either way. Note however that x \in A will not auto-simplify when  *)
-(* A is an explicit simpl_pred T value; the generic simplification rule inE   *)
-(* must be used (when A : pred T, the unfold_in rule can be used). Constants  *)
-(* of type pred T with an explicit simpl_pred value do not auto-simplify when *)
-(* used applicatively, but can still be expanded with inE. This behavior can  *)
-(* be controlled as follows:                                                  *)
-(*   Let A : collective_pred T := [pred x | ... ].                            *)
-(*     The collective_pred T type is just an alias for pred T, but this cast  *)
-(*     stops rewrite inE from expanding the definition of A, thus treating A  *)
-(*     into an abstract collection (unfold_in or in_collective can be used to *)
-(*     expand manually).                                                      *)
-(*   Let A : applicative_pred T := [pred x | ...].                            *)
-(*     This cast causes inE to turn x \in A into the applicative A x form;    *)
-(*     A will then have to unfolded explicitly with the /A rule. This will    *)
-(*     also apply to any definition that reduces to A (e.g., Let B := A).     *)
-(*   Canonical A_app_pred := ApplicativePred A.                               *)
-(*     This declaration, given after definition of A, similarly causes inE to *)
-(*     turn x \in A into A x, but in addition allows the app_predE rule to    *)
-(*     turn A x back into x \in A; it can be used for any definition of type  *)
-(*     pred T, which makes it especially useful for ambivalent predicates     *)
-(*     as the relational transitive closure connect, that are used in both    *)
-(*     applicative and collective styles.                                     *)
-(* Purely for aesthetics, we provide a subtype of collective predicates:      *)
-(*   qualifier q T == a pred T pretty-printing wrapper. An A : qualifier q T  *)
-(*                    coerces to pred_class and thus behaves as a collective  *)
-(*                    predicate, but x \in A and x \notin A are displayed as: *)
-(*             x \is A and x \isn't A when q = 0,                             *)
-(*         x \is a A and x \isn't a A when q = 1,                             *)
-(*       x \is an A and x \isn't an A when q = 2, respectively.               *)
-(*   [qualify x | P] := Qualifier 0 (fun x => P), constructor for the above.  *)
-(* [qualify x : T | P], [qualify a x | P], [qualify an X | P], etc.           *)
-(*                  variants of the above with type constraints and different *)
-(*                  values of q.                                              *)
-(* We provide an internal interface to support attaching properties (such as  *)
-(* being multiplicative) to predicates:                                       *)
-(*    pred_key p == phantom type that will serve as a support for properties  *)
-(*                  to be attached to p : pred_class; instances should be     *)
-(*                  created with Fact/Qed so as to be opaque.                 *)
-(* KeyedPred k_p == an instance of the interface structure that attaches      *)
-(*                  (k_p : pred_key P) to P; the structure projection is a    *)
-(*                  coercion to pred_class.                                   *)
-(* KeyedQualifier k_q == an instance of the interface structure that attaches *)
-(*                  (k_q : pred_key q) to (q : qualifier n T).                *)
-(* DefaultPredKey p == a default value for pred_key p; the vernacular command *)
-(*                  Import DefaultKeying attaches this key to all predicates  *)
-(*                  that are not explicitly keyed.                            *)
-(* Keys can be used to attach properties to predicates, qualifiers and        *)
-(* generic nouns in a way that allows them to be used transparently. The key  *)
-(* projection of a predicate property structure such as unsignedPred should   *)
-(* be a pred_key, not a pred, and corresponding lemmas will have the form     *)
-(*    Lemma rpredN R S (oppS : @opprPred R S) (kS : keyed_pred oppS) :        *)
-(*       {mono -%R: x / x \in kS}.                                            *)
-(* Because x \in kS will be displayed as x \in S (or x \is S, etc), the       *)
-(* canonical instance of opprPred will not normally be exposed (it will also  *)
-(* be erased by /= simplification). In addition each predicate structure      *)
-(* should have a DefaultPredKey Canonical instance that simply issues the     *)
-(* property as a proof obligation (which can be caught by the Prop-irrelevant *)
-(* feature of the ssreflect plugin).                                          *)
-(*   Some properties of predicates and relations:                             *)
-(*                  A =i B <-> A and B are extensionally equivalent.          *)
-(*         {subset A <= B} <-> A is a (collective) subpredicate of B.         *)
-(*             subpred P Q <-> P is an (applicative) subpredicate or Q.       *)
-(*              subrel R S <-> R is a subrelation of S.                       *)
-(* In the following R is in rel T:                                            *)
-(*             reflexive R <-> R is reflexive.                                *)
-(*           irreflexive R <-> R is irreflexive.                              *)
-(*             symmetric R <-> R (in rel T) is symmetric (equation).          *)
-(*         pre_symmetric R <-> R is symmetric (implication).                  *)
-(*         antisymmetric R <-> R is antisymmetric.                            *)
-(*                 total R <-> R is total.                                    *)
-(*            transitive R <-> R is transitive.                               *)
-(*       left_transitive R <-> R is a congruence on its left hand side.       *)
-(*      right_transitive R <-> R is a congruence on its right hand side.      *)
-(*       equivalence_rel R <-> R is an equivalence relation.                  *)
-(* Localization of (Prop) predicates; if P1 is convertible to forall x, Qx,   *)
-(* P2 to forall x y, Qxy and P3 to forall x y z, Qxyz :                       *)
-(*            {for y, P1} <-> Qx{y / x}.                                      *)
-(*             {in A, P1} <-> forall x, x \in A -> Qx.                        *)
-(*       {in A1 & A2, P2} <-> forall x y, x \in A1 -> y \in A2 -> Qxy.        *)
-(*           {in A &, P2} <-> forall x y, x \in A -> y \in A -> Qxy.          *)
-(*  {in A1 & A2 & A3, Q3} <-> forall x y z,                                   *)
-(*                            x \in A1 -> y \in A2 -> z \in A3 -> Qxyz.       *)
-(*     {in A1 & A2 &, Q3} == {in A1 & A2 & A2, Q3}.                           *)
-(*      {in A1 && A3, Q3} == {in A1 & A1 & A3, Q3}.                           *)
-(*          {in A &&, Q3} == {in A & A & A, Q3}.                              *)
-(*    {in A, bijective f} == f has a right inverse in A.                      *)
-(*             {on C, P1} == forall x, (f x) \in C -> Qx                      *)
-(*                           when P1 is also convertible to Pf f.             *)
-(*           {on C &, P2} == forall x y, f x \in C -> f y \in C -> Qxy        *)
-(*                           when P2 is also convertible to Pf f.             *)
-(*        {on C, P1' & g} == forall x, (f x) \in cd -> Qx                     *)
-(*                           when P1' is convertible to Pf f                  *)
-(*                           and P1' g is convertible to forall x, Qx.        *)
-(*    {on C, bijective f} == f has a right inverse on C.                      *)
-(* This file extends the lemma name suffix conventions of ssrfun as follows:  *)
-(*   A -- associativity, as in andbA : associative andb.                      *)
-(*  AC -- right commutativity.                                                *)
-(* ACA -- self-interchange (inner commutativity), e.g.,                       *)
-(*        orbACA : (a || b) || (c || d) = (a || c) || (b || d).               *)
-(*   b -- a boolean argument, as in andbb : idempotent andb.                  *)
-(*   C -- commutativity, as in andbC : commutative andb,                      *)
-(*        or predicate complement, as in predC.                               *)
-(*  CA -- left commutativity.                                                 *)
-(*   D -- predicate difference, as in predD.                                  *)
-(*   E -- elimination, as in negbFE : ~~ b = false -> b.                      *)
-(*   F or f -- boolean false, as in andbF : b && false = false.               *)
-(*   I -- left/right injectivity, as in addbI : right_injective addb,         *)
-(*        or predicate intersection, as in predI.                             *)
-(*   l -- a left-hand operation, as andb_orl : left_distributive andb orb.    *)
-(*   N or n -- boolean negation, as in andbN : a && (~~ a) = false.           *)
-(*   P -- a characteristic property, often a reflection lemma, as in          *)
-(*        andP : reflect (a /\ b) (a && b).                                   *)
-(*   r -- a right-hand operation, as orb_andr : rightt_distributive orb andb. *)
-(*   T or t -- boolean truth, as in andbT: right_id true andb.                *)
-(*   U -- predicate union, as in predU.                                       *)
-(*   W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P.         *)
-(******************************************************************************)
+
+(**  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).
+                            This is just input and displayed as `b''.
+             reflect P b == the reflection inductive predicate, asserting
+                            that the logical proposition P : prop with the
+                            formula b : bool. Lemmas asserting reflect P b
+                            are often referred to as "views".
+  iffP, appP, sameP, rwP :: lemmas for direct manipulation of reflection
+                            views: iffP is used to prove reflection from
+                            logical equivalence, appP to compose views, and
+                            sameP and rwP to perform boolean and setoid
+                            rewriting.
+                   elimT :: coercion reflect >-> Funclass, which allows the
+                            direct application of `reflect' views to
+                            boolean assertions.
+             decidable P <-> P is effectively decidable (:= {P} + {~ P}.
+    contra, contraL, ... :: contraposition lemmas.
+           altP my_viewP :: natural alternative for reflection; given
+                            lemma myviewP: reflect my_Prop my_formula,
+                              have #[#myP | not_myP#]# := altP my_viewP.
+                            generates two subgoals, in which my_formula has
+                            been replaced by true and false, resp., with
+                            new assumptions myP : my_Prop and
+                            not_myP: ~~ my_formula.
+                            Caveat: my_formula must be an APPLICATION, not
+                            a variable, constant, let-in, etc. (due to the
+                            poor behaviour of dependent index matching).
+        boolP my_formula :: boolean disjunction, equivalent to
+                            altP (idP my_formula) but circumventing the
+                            dependent index capture issue; destructing
+                            boolP my_formula generates two subgoals with
+                            assumtions my_formula and ~~ myformula. As
+                            with altP, my_formula must be an application.
+            \unless C, P <-> we can assume property P when a something that
+                            holds under condition C (such as C itself).
+                         := forall G : Prop, (C -> G) -> (P -> G) -> G.
+                            This is just C \/ P or rather its impredicative
+                            encoding, whose usage better fits the above
+                            description: given a lemma UCP whose conclusion
+                            is \unless C, P we can assume P by writing:
+                              wlog hP: / P by apply/UCP; (prove C -> goal).
+                           or even apply: UCP id _ => hP if the goal is C.
+           classically P <-> we can assume P when proving is_true b.
+                         := forall b : bool, (P -> b) -> b.
+                            This is equivalent to ~ (~ P) when P : Prop.
+             implies P Q == wrapper variant type that coerces to P -> Q and
+                            can be used as a P -> Q view unambigously.
+                            Useful to avoid spurious insertion of <-> views
+                            when Q is a conjunction of foralls, as in Lemma
+                            all_and2 below; conversely, avoids confusion in
+                            apply views for impredicative properties, such
+                            as \unless C, P. Also supports contrapositives.
+                  a && b == the boolean conjunction of a and b.
+                  a || b == the boolean disjunction of a and b.
+                 a ==> b == the boolean implication of b by a.
+                    ~~ a == the boolean negation of a.
+                 a (+) b == the boolean exclusive or (or sum) of a and b.
+     #[# /\ P1 , P2 & P3 #]# == multiway logical conjunction, up to 5 terms.
+     #[# \/ P1 , P2 | P3 #]# == multiway logical disjunction, up to 4 terms.
+        #[#&& a, b, c & d#]# == iterated, right associative boolean conjunction
+                            with arbitrary arity.
+        #[#|| a, b, c | d#]# == iterated, right associative boolean disjunction
+                            with arbitrary arity.
+      #[#==> a, b, c => d#]# == iterated, right associative boolean implication
+                            with arbitrary arity.
+              and3P, ... == specific reflection lemmas for iterated
+                            connectives.
+       andTb, orbAC, ... == systematic names for boolean connective
+                            properties (see suffix conventions below).
+              prop_congr == a tactic to move a boolean equality from
+                            its coerced form in Prop to the equality
+                            in bool.
+              bool_congr == resolution tactic for blindly weeding out
+                            like terms from boolean equalities (can fail).
+ This file provides a theory of boolean predicates and relations:
+                  pred T == the type of bool predicates (:= T -> bool).
+            simpl_pred T == the type of simplifying bool predicates, using
+                            the simpl_fun from ssrfun.v.
+                   rel T == the type of bool relations.
+                         := T -> pred T or T -> T -> bool.
+             simpl_rel T == type of simplifying relations.
+                predType == the generic predicate interface, supported for
+                            for lists and sets.
+              pred_class == a coercion class for the predType projection to
+                            pred; declaring a coercion to pred_class is an
+                            alternative way of equipping a type with a
+                            predType structure, which interoperates better
+                            with coercion subtyping. This is used, e.g.,
+                            for finite sets, so that finite groups inherit
+                            the membership operation by coercing to sets.
+ If P is a predicate the proposition "x satisfies P" can be written
+ applicatively as (P x), or using an explicit connective as (x \in P); in
+ the latter case we say that P is a "collective" predicate. We use A, B
+ rather than P, Q for collective predicates:
+                 x \in A == x satisfies the (collective) predicate A.
+              x \notin A == x doesn't satisfy the (collective) predicate A.
+ The pred T type can be used as a generic predicate type for either kind,
+ but the two kinds of predicates should not be confused. When a "generic"
+ pred T value of one type needs to be passed as the other the following
+ conversions should be used explicitly:
+             SimplPred P == a (simplifying) applicative equivalent of P.
+                   mem A == an applicative equivalent of A:
+                            mem A x simplifies to x \in A.
+ Alternatively one can use the syntax for explicit simplifying predicates
+ and relations (in the following x is bound in E):
+            #[#pred x | E#]# == simplifying (see ssrfun) predicate x => E.
+        #[#pred x : T | E#]# == predicate x => E, with a cast on the argument.
+          #[#pred : T | P#]# == constant predicate P on type T.
+      #[#pred x | E1 & E2#]# == #[#pred x | E1 && E2#]#; an x : T cast is allowed.
+           #[#pred x in A#]# == #[#pred x | x in A#]#.
+       #[#pred x in A | E#]# == #[#pred x | x in A & E#]#.
+ #[#pred x in A | E1 & E2#]# == #[#pred x in A | E1 && E2#]#.
+           #[#predU A & B#]# == union of two collective predicates A and B.
+           #[#predI A & B#]# == intersection of collective predicates A and B.
+           #[#predD A & B#]# == difference of collective predicates A and B.
+               #[#predC A#]# == complement of the collective predicate A.
+          #[#preim f of A#]# == preimage under f of the collective predicate A.
+          predU P Q, ... == union, etc of applicative predicates.
+                   pred0 == the empty predicate.
+                   predT == the total (always true) predicate.
+                            if T : predArgType, then T coerces to predT.
+                   {: T} == T cast to predArgType (e.g., {: bool * nat})
+ In the following, x and y are bound in E:
+           #[#rel x y | E#]# == simplifying relation x, y => E.
+       #[#rel x y : T | E#]# == simplifying relation with arguments cast.
+  #[#rel x y in A & B | E#]# == #[#rel x y | #[#&& x \in A, y \in B & E#]# #]#.
+      #[#rel x y in A & B#]# == #[#rel x y | (x \in A) && (y \in B) #]#.
+      #[#rel x y in A | E#]# == #[#rel x y in A & A | E#]#.
+          #[#rel x y in A#]# == #[#rel x y in A & A#]#.
+                relU R S == union of relations R and S.
+ Explicit values of type pred T (i.e., lamdba terms) should always be used
+ applicatively, while values of collection types implementing the predType
+ interface, such as sequences or sets should always be used as collective
+ predicates. Defined constants and functions of type pred T or simpl_pred T
+ as well as the explicit simpl_pred T values described below, can generally
+ be used either way. Note however that x \in A will not auto-simplify when
+ A is an explicit simpl_pred T value; the generic simplification rule inE
+ must be used (when A : pred T, the unfold_in rule can be used). Constants
+ of type pred T with an explicit simpl_pred value do not auto-simplify when
+ used applicatively, but can still be expanded with inE. This behavior can
+ be controlled as follows:
+   Let A : collective_pred T := #[#pred x | ... #]#.
+     The collective_pred T type is just an alias for pred T, but this cast
+     stops rewrite inE from expanding the definition of A, thus treating A
+     into an abstract collection (unfold_in or in_collective can be used to
+     expand manually).
+   Let A : applicative_pred T := #[#pred x | ... #]#.
+     This cast causes inE to turn x \in A into the applicative A x form;
+     A will then have to unfolded explicitly with the /A rule. This will
+     also apply to any definition that reduces to A (e.g., Let B := A).
+   Canonical A_app_pred := ApplicativePred A.
+     This declaration, given after definition of A, similarly causes inE to
+     turn x \in A into A x, but in addition allows the app_predE rule to
+     turn A x back into x \in A; it can be used for any definition of type
+     pred T, which makes it especially useful for ambivalent predicates
+     as the relational transitive closure connect, that are used in both
+     applicative and collective styles.
+ Purely for aesthetics, we provide a subtype of collective predicates:
+   qualifier q T == a pred T pretty-printing wrapper. An A : qualifier q T
+                    coerces to pred_class and thus behaves as a collective
+                    predicate, but x \in A and x \notin A are displayed as:
+             x \is A and x \isn't A when q = 0,
+         x \is a A and x \isn't a A when q = 1,
+       x \is an A and x \isn't an A when q = 2, respectively.
+   #[#qualify x | P#]# := Qualifier 0 (fun x => P), constructor for the above.
+ #[#qualify x : T | P#]#, #[#qualify a x | P#]#, #[#qualify an X | P#]#, etc.
+                  variants of the above with type constraints and different
+                  values of q.
+ We provide an internal interface to support attaching properties (such as
+ being multiplicative) to predicates:
+    pred_key p == phantom type that will serve as a support for properties
+                  to be attached to p : pred_class; instances should be
+                  created with Fact/Qed so as to be opaque.
+ KeyedPred k_p == an instance of the interface structure that attaches
+                  (k_p : pred_key P) to P; the structure projection is a
+                  coercion to pred_class.
+ KeyedQualifier k_q == an instance of the interface structure that attaches
+                  (k_q : pred_key q) to (q : qualifier n T).
+ DefaultPredKey p == a default value for pred_key p; the vernacular command
+                  Import DefaultKeying attaches this key to all predicates
+                  that are not explicitly keyed.
+ Keys can be used to attach properties to predicates, qualifiers and
+ generic nouns in a way that allows them to be used transparently. The key
+ projection of a predicate property structure such as unsignedPred should
+ be a pred_key, not a pred, and corresponding lemmas will have the form
+    Lemma rpredN R S (oppS : @opprPred R S) (kS : keyed_pred oppS) :
+       {mono -%%R: x / x \in kS}.
+ Because x \in kS will be displayed as x \in S (or x \is S, etc), the
+ canonical instance of opprPred will not normally be exposed (it will also
+ be erased by /= simplification). In addition each predicate structure
+ should have a DefaultPredKey Canonical instance that simply issues the
+ property as a proof obligation (which can be caught by the Prop-irrelevant
+ feature of the ssreflect plugin).
+   Some properties of predicates and relations:
+                  A =i B <-> A and B are extensionally equivalent.
+         {subset A <= B} <-> A is a (collective) subpredicate of B.
+             subpred P Q <-> P is an (applicative) subpredicate or Q.
+              subrel R S <-> R is a subrelation of S.
+ In the following R is in rel T:
+             reflexive R <-> R is reflexive.
+           irreflexive R <-> R is irreflexive.
+             symmetric R <-> R (in rel T) is symmetric (equation).
+         pre_symmetric R <-> R is symmetric (implication).
+         antisymmetric R <-> R is antisymmetric.
+                 total R <-> R is total.
+            transitive R <-> R is transitive.
+       left_transitive R <-> R is a congruence on its left hand side.
+      right_transitive R <-> R is a congruence on its right hand side.
+       equivalence_rel R <-> R is an equivalence relation.
+ Localization of (Prop) predicates; if P1 is convertible to forall x, Qx,
+ P2 to forall x y, Qxy and P3 to forall x y z, Qxyz :
+            {for y, P1} <-> Qx{y / x}.
+             {in A, P1} <-> forall x, x \in A -> Qx.
+       {in A1 & A2, P2} <-> forall x y, x \in A1 -> y \in A2 -> Qxy.
+           {in A &, P2} <-> forall x y, x \in A -> y \in A -> Qxy.
+  {in A1 & A2 & A3, Q3} <-> forall x y z,
+                            x \in A1 -> y \in A2 -> z \in A3 -> Qxyz.
+     {in A1 & A2 &, Q3} == {in A1 & A2 & A2, Q3}.
+      {in A1 && A3, Q3} == {in A1 & A1 & A3, Q3}.
+          {in A &&, Q3} == {in A & A & A, Q3}.
+    {in A, bijective f} == f has a right inverse in A.
+             {on C, P1} == forall x, (f x) \in C -> Qx
+                           when P1 is also convertible to Pf f.
+           {on C &, P2} == forall x y, f x \in C -> f y \in C -> Qxy
+                           when P2 is also convertible to Pf f.
+        {on C, P1' & g} == forall x, (f x) \in cd -> Qx
+                           when P1' is convertible to Pf f
+                           and P1' g is convertible to forall x, Qx.
+    {on C, bijective f} == f has a right inverse on C.
+ This file extends the lemma name suffix conventions of ssrfun as follows:
+   A -- associativity, as in andbA : associative andb.
+  AC -- right commutativity.
+ ACA -- self-interchange (inner commutativity), e.g.,
+        orbACA : (a || b) || (c || d) = (a || c) || (b || d).
+   b -- a boolean argument, as in andbb : idempotent andb.
+   C -- commutativity, as in andbC : commutative andb,
+        or predicate complement, as in predC.
+  CA -- left commutativity.
+   D -- predicate difference, as in predD.
+   E -- elimination, as in negbFE : ~~ b = false -> b.
+   F or f -- boolean false, as in andbF : b && false = false.
+   I -- left/right injectivity, as in addbI : right_injective addb,
+        or predicate intersection, as in predI.
+   l -- a left-hand operation, as andb_orl : left_distributive andb orb.
+   N or n -- boolean negation, as in andbN : a && (~~ a) = false.
+   P -- a characteristic property, often a reflection lemma, as in
+        andP : reflect (a /\ b) (a && b).
+   r -- a right-hand operation, as orb_andr : rightt_distributive orb andb.
+   T or t -- boolean truth, as in andbT: right_id true andb.
+   U -- predicate union, as in predU.
+   W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P.          **)
+
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -288,23 +288,23 @@ 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  *)
-(* format, namely                                                             *)
-(*    [op arg1, arg2, ... last_separator last_arg]                            *)
-(* This usually denotes a right-associative applications of op, e.g.,         *)
-(*  [&& a, b, c & d] denotes a && (b && (c && d))                             *)
-(* The last_separator must be a non-operator token. Here we use &, | or =>;   *)
-(* our default is &, but we try to match the intended meaning of op. The      *)
-(* separator is a workaround for limitations of the parsing engine; the same  *)
-(* limitations mean the separator cannot be omitted even when last_arg can.   *)
-(*   The Notation declarations are complicated by the separate treatment for  *)
-(* some fixed arities (binary for bool operators, and all arities for Prop    *)
-(* operators).                                                                *)
-(*   We also use the square brackets in comprehension-style notations         *)
-(*    [type var separator expr]                                               *)
-(* where "type" is the type of the comprehension (e.g., pred) and "separator" *)
-(* is | or => . It is important that in other notations a leading square      *)
-(* bracket [ is always followed by an operator symbol or a fixed identifier.  *)
+(**  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.,
+  #[#&& a, b, c & d#]# denotes a && (b && (c && d))
+ The last_separator must be a non-operator token. Here we use &, | or =>;
+ our default is &, but we try to match the intended meaning of op. The
+ separator is a workaround for limitations of the parsing engine; the same
+ limitations mean the separator cannot be omitted even when last_arg can.
+   The Notation declarations are complicated by the separate treatment for
+ some fixed arities (binary for bool operators, and all arities for Prop
+ operators).
+   We also use the square brackets in comprehension-style notations
+    #[#type var separator expr#]#
+ where "type" is the type of the comprehension (e.g., pred) and "separator"
+ is | or => . It is important that in other notations a leading square
+ bracket #[# is always followed by an operator symbol or a fixed identifier.   **)
 
 Reserved Notation "[ /\ P1 & P2 ]" (at level 0, only parsing).
 Reserved Notation "[ /\ P1 , P2 & P3 ]" (at level 0, format
@@ -344,19 +344,19 @@ Reserved Notation "[ 'rel' x y => E ]" (at level 0, x, y at level 8, format
 Reserved Notation "[ 'rel' x y : T => E ]" (at level 0, x, y at level 8, format
   "'[hv' [ 'rel'  x  y :  T  => '/ '  E ] ']'").
 
-(* Shorter delimiter *)
+(**  Shorter delimiter  **)
 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. *)
+(**  Notation for && and || is declared in Init.Datatypes.  **)
 Notation "~~ b" := (negb b) : bool_scope.
 Notation "b ==> c" := (implb b c) : bool_scope.
 Notation "b1 (+) b2" := (addb b1 b2) : bool_scope.
 
-(* Constant is_true b := b = true is defined in Init.Datatypes. *)
+(**  Constant is_true b := b = true is defined in Init.Datatypes.  **)
 Coercion is_true : bool >-> Sortclass. (* Prop *)
 
 Lemma prop_congr : forall b b' : bool, b = b' -> b = b' :> Prop.
@@ -364,21 +364,21 @@ Proof. by move=> b b' ->. Qed.
 
 Ltac prop_congr := apply: prop_congr.
 
-(* Lemmas for trivial. *)
+(**  Lemmas for trivial.  **)
 Lemma is_true_true : true.               Proof. by []. Qed.
 Lemma not_false_is_true : ~ false.       Proof. by []. Qed.
 Lemma is_true_locked_true : locked true. Proof. by unlock. Qed.
 Hint Resolve is_true_true not_false_is_true is_true_locked_true.
 
-(* Shorter names. *)
+(**  Shorter names.  **)
 Definition isT := is_true_true.
 Definition notF := not_false_is_true.
 
-(* Negation lemmas. *)
+(**  Negation lemmas.  **)
 
-(* 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.                                            *)
+(**  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.                                             **)
 
 Lemma negbT b : b = false -> ~~ b.          Proof. by case: b. Qed.
 Lemma negbTE b : ~~ b -> b = false.         Proof. by case: b. Qed.
@@ -426,8 +426,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 *)
-(* to use ssr's boolean if rather than Coq's "generic" if.            *)
+(**  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,16 +441,16 @@ 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  *)
-(* condition without repeating it inside the proof (the latter IS         *)
-(* preferable when the condition is short).                               *)
-(* Usage :                                                                *)
-(*   if the goal contains (if cond then ...) = ...                        *)
-(*     case: ifP => Hcond.                                                *)
-(*   generates two subgoal, with the assumption Hcond : cond = true/false *)
-(*     Rewrite if_same  eliminates redundant ifs                          *)
-(*     Rewrite (fun_if f) moves a function f inside an if                 *)
-(*     Rewrite if_arg moves an argument inside a function-valued if       *)
+(**  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 :
+   if the goal contains (if cond then ...) = ...
+     case: ifP => Hcond.
+   generates two subgoal, with the assumption Hcond : cond = true/false
+     Rewrite if_same  eliminates redundant ifs
+     Rewrite (fun_if f) moves a function f inside an if
+     Rewrite if_arg moves an argument inside a function-valued if        **)
 
 Section BoolIf.
 
@@ -483,13 +483,13 @@ 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.
 
 End BoolIf.
 
-(* Core (internal) reflection lemmas, used for the three kinds of views. *)
+(**  Core (internal) reflection lemmas, used for the three kinds of views.  **)
 
 Section ReflectCore.
 
@@ -517,7 +517,7 @@ Proof. by case Hb => [? _ H ? | ? H _]; case: H. Qed.
 
 End ReflectCore.
 
-(* Internal negated reflection lemmas *)
+(**  Internal negated reflection lemmas  **)
 Section ReflectNegCore.
 
 Variables (P Q : Prop) (b c : bool).
@@ -537,7 +537,7 @@ Proof. by rewrite -if_neg; apply: xorPif. Qed.
 
 End ReflectNegCore.
 
-(* User-oriented reflection lemmas *)
+(**  User-oriented reflection lemmas  **)
 Section Reflect.
 
 Variables (P Q : Prop) (b b' c : bool).
@@ -584,7 +584,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.
@@ -600,7 +600,7 @@ Hint View for apply/ introTF|3 introNTF|3 introTFn|3 elimT|2 elimTn|2 elimN|2.
 
 Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3.
 
-(* Allow the direct application of a reflection lemma to a boolean assertion. *)
+(**  Allow the direct application of a reflection lemma to a boolean assertion.  **)
 Coercion elimT : reflect >-> Funclass.
 
 Variant implies P Q := Implies of P -> Q.
@@ -611,7 +611,7 @@ Coercion impliesP : implies >-> Funclass.
 Hint View for move/ impliesPn|2 impliesP|2.
 Hint View for apply/ impliesPn|2 impliesP|2.
 
-(* Impredicative or, which can emulate a classical not-implies. *)
+(**  Impredicative or, which can emulate a classical not-implies.  **)
 Definition unless condition property : Prop :=
  forall goal : Prop, (condition -> goal) -> (property -> goal) -> goal.
 
@@ -637,8 +637,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.      *)
-(* Note that we cannot use "unless" here for lack of universe polymorphism.   *)
+(**  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.
 
 Lemma classicP (P : Prop) : classically P <-> ~ ~ P.
@@ -669,11 +669,11 @@ 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    *)
-(* 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 *)
-(* associativity of list expressions and thus more convenient in most proofs. *)
+(**  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
+ associativity of list expressions and thus more convenient in most proofs.  **)
 
 Inductive and3 (P1 P2 P3 : Prop) : Prop := And3 of P1 & P2 & P3.
 
@@ -822,7 +822,7 @@ Arguments implyP [b1 b2].
 Prenex Implicits idP idPn negP negPn negPf.
 Prenex Implicits andP and3P and4P and5P orP or3P or4P nandP norP implyP.
 
-(* Shorter, more systematic names for the boolean connectives laws.       *)
+(**  Shorter, more systematic names for the boolean connectives laws.        **)
 
 Lemma andTb : left_id true andb.       Proof. by []. Qed.
 Lemma andFb : left_zero false andb.    Proof. by []. Qed.
@@ -880,14 +880,14 @@ Proof. by case: a; case: b. Qed.
 Lemma negb_or (a b : bool) : ~~ (a || b) = ~~ a && ~~ b.
 Proof. by case: a; case: b. Qed.
 
-(* Pseudo-cancellation -- i.e, absorbtion *)
+(**  Pseudo-cancellation -- i.e, absorbtion  **)
 
 Lemma andbK a b : a && b || a = a.  Proof. by case: a; case: b. Qed.
 Lemma andKb a b : a || b && a = a.  Proof. by case: a; case: b. Qed.
 Lemma orbK a b : (a || b) && a = a. Proof. by case: a; case: b. Qed.
 Lemma orKb a b : a && (b || a) = a. Proof. by case: a; case: b. Qed.
 
-(* Imply *)
+(**  Imply  **)
 
 Lemma implybT b : b ==> true.           Proof. by case: b. Qed.
 Lemma implybF b : (b ==> false) = ~~ b. Proof. by case: b. Qed.
@@ -917,7 +917,7 @@ Proof. by case: a; case: b => // ->. Qed.
 Lemma implyb_id2l (a b c : bool) : (a -> b = c) -> (a ==> b) = (a ==> c).
 Proof. by case: a; case: b; case: c => // ->. Qed.
 
-(* Addition (xor) *)
+(**  Addition (xor)  **)
 
 Lemma addFb : left_id false addb.               Proof. by []. Qed.
 Lemma addbF : right_id false addb.              Proof. by case. Qed.
@@ -946,9 +946,9 @@ 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       *)
-(* 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!            *)
+(**  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!             **)
 
 Ltac bool_congr :=
   match goal with
@@ -963,100 +963,100 @@ Ltac bool_congr :=
   | |- (~~ ?X1 = ?X2) => congr 1 negb
   end.
 
-(******************************************************************************)
-(* 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 *)
-(* and collective, based on the syntax used to test them at some x in T:      *)
-(* - For an applicative predicate P, one uses prefix syntax:                  *)
-(*     P x                                                                    *)
-(*   Also, most operations on applicative predicates use prefix syntax as     *)
-(*   well (e.g., predI P Q).                                                  *)
-(* - For a collective predicate A, one uses infix syntax:                     *)
-(*     x \in A                                                                *)
-(*   and all operations on collective predicates use infix syntax as well     *)
-(*   (e.g., [predI A & B]).                                                   *)
-(* There are only two kinds of applicative predicates:                        *)
-(* - pred T, the alias for T -> bool mentioned above                          *)
-(* - simpl_pred T, an alias for simpl_fun T bool with a coercion to pred T    *)
-(*   that auto-simplifies on application (see ssrfun).                        *)
-(* On the other hand, the set of collective predicate types is open-ended via *)
-(* - predType T, a Structure that can be used to put Canonical collective     *)
-(*   predicate interpretation on other types, such as lists, tuples,          *)
-(*   finite sets, etc.                                                        *)
-(* Indeed, we define such interpretations for applicative predicate types,    *)
-(* which can therefore also be used with the infix syntax, e.g.,              *)
-(*     x \in predI P Q                                                        *)
-(* Moreover these infix forms are convertible to their prefix counterpart     *)
-(* (e.g., predI P Q x which in turn simplifies to P x && Q x). The converse   *)
-(* is not true, however; collective predicate types cannot, in general, be    *)
-(* general, be used applicatively, because of the "uniform inheritance"       *)
-(* restriction on implicit coercions.                                         *)
-(*   However, we do define an explicit generic coercion                       *)
-(* - mem : forall (pT : predType), pT -> mem_pred T                           *)
-(*   where mem_pred T is a variant of simpl_pred T that preserves the infix   *)
-(*   syntax, i.e., mem A x auto-simplifies to x \in A.                        *)
-(* Indeed, the infix "collective" operators are notation for a prefix         *)
-(* operator with arguments of type mem_pred T or pred T, applied to coerced   *)
-(* collective predicates, e.g.,                                               *)
-(*      Notation "x \in A" := (in_mem x (mem A)).                             *)
-(* This prevents the variability in the predicate type from interfering with  *)
-(* the application of generic lemmas. Moreover this also makes it much easier *)
-(* to define generic lemmas, because the simplest type -- pred T -- can be    *)
-(* used as the type of generic collective predicates, provided one takes care *)
-(* not to use it applicatively; this avoids the burden of having to declare a *)
-(* different predicate type for each predicate parameter of each section or   *)
-(* lemma.                                                                     *)
-(*   This trick is made possible by the fact that the constructor of the      *)
-(* mem_pred T type aligns the unification process, forcing a generic          *)
-(* "collective" predicate A : pred T to unify with the actual collective B,   *)
-(* which mem has coerced to pred T via an internal, hidden implicit coercion, *)
-(* supplied by the predType structure for B. Users should take care not to    *)
-(* inadvertently "strip" (mem B) down to the coerced B, since this will       *)
-(* expose the internal coercion: Coq will display a term B x that cannot be   *)
-(* typed as such. The topredE lemma can be used to restore the x \in B        *)
-(* syntax in this case. While -topredE can conversely be used to change       *)
-(* x \in P into P x, it is safer to use the inE and memE lemmas instead, as   *)
-(* they do not run the risk of exposing internal coercions. As a consequence  *)
-(* it is better to explicitly cast a generic applicative pred T to simpl_pred *)
-(* using the SimplPred constructor, when it is used as a collective predicate *)
-(* (see, e.g., Lemma eq_big in bigop).                                        *)
-(*   We also sometimes "instantiate" the predType structure by defining a     *)
-(* coercion to the sort of the predPredType structure. This works better for  *)
-(* types such as {set T} that have subtypes that coerce to them, since the    *)
-(* same coercion will be inserted by the application of mem. It also lets us  *)
-(* turn any Type aT : predArgType into the total predicate over that type,    *)
-(* i.e., fun _: aT => true. This allows us to write, e.g., #|'I_n| for the    *)
-(* cardinal of the (finite) type of integers less than n.                     *)
-(*   Collective predicates have a specific extensional equality,              *)
-(*   - A =i B,                                                                *)
-(* while applicative predicates use the extensional equality of functions,    *)
-(*   - P =1 Q                                                                 *)
-(* The two forms are convertible, however.                                    *)
-(* We lift boolean operations to predicates, defining:                        *)
-(* - predU (union), predI (intersection), predC (complement),                 *)
-(*   predD (difference), and preim (preimage, i.e., composition)              *)
-(* For each operation we define three forms, typically:                       *)
-(* - predU : pred T -> pred T -> simpl_pred T                                 *)
-(* - [predU A & B], a Notation for predU (mem A) (mem B)                      *)
-(* - xpredU, a Notation for the lambda-expression inside predU,               *)
-(*     which is mostly useful as an argument of =1, since it exposes the head *)
-(*     head constant of the expression to the ssreflect matching algorithm.   *)
-(* The syntax for the preimage of a collective predicate A is                 *)
-(* - [preim f of A]                                                           *)
-(* Finally, the generic syntax for defining a simpl_pred T is                 *)
-(* - [pred x : T | P(x)], [pred x | P(x)], [pred x in A | P(x)], etc.         *)
-(* We also support boolean relations, but only the applicative form, with     *)
-(* types                                                                      *)
-(* - rel T, an alias for T -> pred T                                          *)
-(* - simpl_rel T, an auto-simplifying version, and syntax                     *)
-(*   [rel x y | P(x,y)], [rel x y in A & B | P(x,y)], etc.                    *)
-(* The notation [rel of fA] can be used to coerce a function returning a      *)
-(* collective predicate to one returning pred T.                              *)
-(*   Finally, note that there is specific support for ambivalent predicates   *)
-(* that can work in either style, as per this file's head descriptor.         *)
-(******************************************************************************)
+
+(**  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
+ and collective, based on the syntax used to test them at some x in T:
+ - For an applicative predicate P, one uses prefix syntax:
+     P x
+   Also, most operations on applicative predicates use prefix syntax as
+   well (e.g., predI P Q).
+ - For a collective predicate A, one uses infix syntax:
+     x \in A
+   and all operations on collective predicates use infix syntax as well
+   (e.g., #[#predI A & B#]#).
+ There are only two kinds of applicative predicates:
+ - pred T, the alias for T -> bool mentioned above
+ - simpl_pred T, an alias for simpl_fun T bool with a coercion to pred T
+   that auto-simplifies on application (see ssrfun).
+ On the other hand, the set of collective predicate types is open-ended via
+ - predType T, a Structure that can be used to put Canonical collective
+   predicate interpretation on other types, such as lists, tuples,
+   finite sets, etc.
+ Indeed, we define such interpretations for applicative predicate types,
+ which can therefore also be used with the infix syntax, e.g.,
+     x \in predI P Q
+ Moreover these infix forms are convertible to their prefix counterpart
+ (e.g., predI P Q x which in turn simplifies to P x && Q x). The converse
+ is not true, however; collective predicate types cannot, in general, be
+ general, be used applicatively, because of the "uniform inheritance"
+ restriction on implicit coercions.
+   However, we do define an explicit generic coercion
+ - mem : forall (pT : predType), pT -> mem_pred T
+   where mem_pred T is a variant of simpl_pred T that preserves the infix
+   syntax, i.e., mem A x auto-simplifies to x \in A.
+ Indeed, the infix "collective" operators are notation for a prefix
+ operator with arguments of type mem_pred T or pred T, applied to coerced
+ collective predicates, e.g.,
+      Notation "x \in A" := (in_mem x (mem A)).
+ This prevents the variability in the predicate type from interfering with
+ the application of generic lemmas. Moreover this also makes it much easier
+ to define generic lemmas, because the simplest type -- pred T -- can be
+ used as the type of generic collective predicates, provided one takes care
+ not to use it applicatively; this avoids the burden of having to declare a
+ different predicate type for each predicate parameter of each section or
+ lemma.
+   This trick is made possible by the fact that the constructor of the
+ mem_pred T type aligns the unification process, forcing a generic
+ "collective" predicate A : pred T to unify with the actual collective B,
+ which mem has coerced to pred T via an internal, hidden implicit coercion,
+ supplied by the predType structure for B. Users should take care not to
+ inadvertently "strip" (mem B) down to the coerced B, since this will
+ expose the internal coercion: Coq will display a term B x that cannot be
+ typed as such. The topredE lemma can be used to restore the x \in B
+ syntax in this case. While -topredE can conversely be used to change
+ x \in P into P x, it is safer to use the inE and memE lemmas instead, as
+ they do not run the risk of exposing internal coercions. As a consequence
+ it is better to explicitly cast a generic applicative pred T to simpl_pred
+ using the SimplPred constructor, when it is used as a collective predicate
+ (see, e.g., Lemma eq_big in bigop).
+   We also sometimes "instantiate" the predType structure by defining a
+ coercion to the sort of the predPredType structure. This works better for
+ types such as {set T} that have subtypes that coerce to them, since the
+ same coercion will be inserted by the application of mem. It also lets us
+ turn any Type aT : predArgType into the total predicate over that type,
+ i.e., fun _: aT => true. This allows us to write, e.g., ##|'I_n| for the
+ cardinal of the (finite) type of integers less than n.
+   Collective predicates have a specific extensional equality,
+   - A =i B,
+ while applicative predicates use the extensional equality of functions,
+   - P =1 Q
+ The two forms are convertible, however.
+ We lift boolean operations to predicates, defining:
+ - predU (union), predI (intersection), predC (complement),
+   predD (difference), and preim (preimage, i.e., composition)
+ For each operation we define three forms, typically:
+ - predU : pred T -> pred T -> simpl_pred T
+ - #[#predU A & B#]#, a Notation for predU (mem A) (mem B)
+ - xpredU, a Notation for the lambda-expression inside predU,
+     which is mostly useful as an argument of =1, since it exposes the head
+     head constant of the expression to the ssreflect matching algorithm.
+ The syntax for the preimage of a collective predicate A is
+ - #[#preim f of A#]#
+ Finally, the generic syntax for defining a simpl_pred T is
+ - #[#pred x : T | P(x) #]#, #[#pred x | P(x) #]#, #[#pred x in A | P(x) #]#, etc.
+ We also support boolean relations, but only the applicative form, with
+ types
+ - rel T, an alias for T -> pred T
+ - simpl_rel T, an auto-simplifying version, and syntax
+   #[#rel x y | P(x,y) #]#, #[#rel x y in A & B | P(x,y) #]#, etc.
+ The notation #[#rel of fA#]# can be used to coerce a function returning a
+ collective predicate to one returning pred T.
+   Finally, note that there is specific support for ambivalent predicates
+ that can work in either style, as per this file's head descriptor.          **)
+
 
 Definition pred T := T -> bool.
 
@@ -1094,8 +1094,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 *)
-(* collective_of_simpl is not. *)
+(**  Note: applicative_of_simpl is convertible to pred_of_simpl, while
+ collective_of_simpl is not.  **)
 
 Definition pred0 := SimplPred xpred0.
 Definition predT := SimplPred xpredT.
@@ -1166,19 +1166,19 @@ 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    *)
-(* 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  *)
-(* coercion will never be used directly for simpl_pred, since the canonical  *)
-(* instance should always be resolved.                                       *)
+(**  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
+ coercion will never be used directly for simpl_pred, since the canonical
+ instance should always be resolved.                                        **)
 
 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.    *)
-(* Unfortunately, this won't work for existing types like bool, unless we     *)
-(* redefine bool, true, false and all bool ops.                               *)
+(**  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.
 Bind Scope type_scope with predArgType.
 Identity Coercion sort_of_predArgType : predArgType >-> Sortclass.
@@ -1187,8 +1187,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        *)
-(* nosimpl tag.                                                               *)
+(**  These must be defined outside a Section because "cooking" kills the
+ nosimpl tag.                                                                **)
 
 Definition mem T (pT : predType T) : pT -> mem_pred T :=
   nosimpl (let: @PredType _ _ _ (exist _ mem _) := pT return pT -> _ in mem).
@@ -1254,12 +1254,12 @@ 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     *)
-(* 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     *)
-(* projections and overwriting of a variable assignment by a later            *)
-(* unification (probably due to conversion cache cross-talk).                 *)
+(**  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
+ projections and overwriting of a variable assignment by a later
+ unification (probably due to conversion cache cross-talk).                  **)
 Structure manifest_applicative_pred p := ManifestApplicativePred {
   manifest_applicative_pred_value :> pred T;
   _ : manifest_applicative_pred_value = p
@@ -1305,10 +1305,10 @@ 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    *)
-(* 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.                                                         *)
+(**  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.                                                          **)
 Lemma unfold_in x p : (x \in ([eta p] : pred T)) = p x.
 Proof. by []. Qed.
 
@@ -1327,7 +1327,7 @@ Proof. by rewrite -mem_topred. Qed.
 
 End simpl_mem.
 
-(* Qualifiers and keyed predicates. *)
+(**  Qualifiers and keyed predicates.  **)
 
 Variant qualifier (q : nat) T := Qualifier of predPredType T.
 
@@ -1371,7 +1371,7 @@ Notation "[ 'qualify' 'an' x | P ]" := (Qualifier 2 (fun x => P%B))
 Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T => P%B))
   (at level 0, x at level 99, only parsing) : form_scope.
 
-(* Keyed predicates: support for property-bearing predicate interfaces. *)
+(**  Keyed predicates: support for property-bearing predicate interfaces.  **)
 
 Section KeyPred.
 
@@ -1388,13 +1388,13 @@ 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  *)
-(* 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     *)
-(* simpl_of_mem; pred_of_simpl is the mem >-> pred >=> Funclass coercion. We  *)
-(* must write down the coercions explicitly as the Canonical head constant    *)
-(* computation does not strip casts !!                                        *)
+(**  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
+ simpl_of_mem; pred_of_simpl is the mem >-> pred >=> Funclass coercion. We
+ must write down the coercions explicitly as the Canonical head constant
+ computation does not strip casts !!                                         **)
 Canonical keyed_mem :=
   @PackKeyedPred k (pred_of_mem (mem k_p)) keyed_predE.
 Canonical keyed_mem_simpl :=
@@ -1434,7 +1434,7 @@ Canonical default_keyed_qualifier T n (q : qualifier n T) :=
 
 End DefaultKeying.
 
-(* Skolemizing with conditions. *)
+(**  Skolemizing with conditions.  **)
 
 Lemma all_tag_cond_dep I T (C : pred I) U :
     (forall x, T x) -> (forall x, C x -> {y : T x & U x y}) ->
@@ -1461,8 +1461,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  *)
-(* will not expand the constant.                                              *)
+(**  Caveat: reflexive should not be used to state lemmas, as auto and trivial
+ will not expand the constant.                                               **)
 
 Variable T : Type.
 
@@ -1496,8 +1496,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   *)
-(* can be localized using the {in ..., ..} form defined below.                *)
+(**  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).
 
@@ -1512,7 +1512,7 @@ End RelationProperties.
 Lemma rev_trans T (R : rel T) : transitive R -> transitive (fun x y => R y x).
 Proof. by move=> trR x y z Ryx Rzy; apply: trR Rzy Ryx. Qed.
 
-(* Property localization *)
+(**  Property localization  **)
 
 Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0).
 Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0).
@@ -1626,11 +1626,11 @@ 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.                *)
-(* 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  *)
-(* of the ssrfun 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
+ of the ssrfun predicates.                                                   **)
 
 Section LocalGlobal.
 
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index e43cab094b..3bd86063d7 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -14,46 +14,46 @@ Require Import Bool. (* For bool_scope delimiter 'bool'. *)
 Require Import ssrmatching.
 Declare ML Module "ssreflect_plugin".
 
-(******************************************************************************)
-(* 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    *)
-(* advanced developers; in addition the following are defined:                *)
-(*   [the str of v by f] == the Canonical s : str such that f s = v.          *)
-(*        [the str of v] == the Canonical s : str that coerces to v.          *)
-(*        argumentType c == the T such that c : forall x : T, P x.            *)
-(*          returnType c == the R such that c : T -> R.                       *)
-(*     {type of c for s} == P s where c : forall x : T, P x.                  *)
-(*           phantom T v == singleton type with inhabitant Phantom T v.       *)
-(*               phant T == singleton type with inhabitant Phant v.           *)
-(*                 =^~ r == the converse of rewriting rule r (e.g., in a      *)
-(*                          rewrite multirule).                               *)
-(*             unkeyed t == t, but treated as an unkeyed matching pattern by  *)
-(*                          the ssreflect matching algorithm.                 *)
-(*             nosimpl t == t, but on the right-hand side of Definition C :=  *)
-(*                          nosimpl disables expansion of C by /=.            *)
-(*              locked t == t, but locked t is not convertible to t.          *)
-(*       locked_with k t == t, but not convertible to t or locked_with k' t   *)
-(*                          unless k = k' (with k : unit). Coq type-checking  *)
-(*                          will be much more efficient if locked_with with a *)
-(*                          bespoke k is used for sealed definitions.         *)
-(*          unlockable v == interface for sealed constant definitions of v.   *)
-(*        Unlockable def == the unlockable that registers def : C = v.        *)
-(*     [unlockable of C] == a clone for C of the canonical unlockable for the *)
-(*                          definition of C (e.g., if it uses locked_with).   *)
-(*    [unlockable fun C] == [unlockable of C] with the expansion forced to be *)
-(*                          an explicit lambda expression.                    *)
-(*  -> The usage pattern for ADT operations is:                               *)
-(*       Definition foo_def x1 .. xn := big_foo_expression.                   *)
-(*       Fact foo_key : unit. Proof. by []. Qed.                              *)
-(*       Definition foo := locked_with foo_key foo_def.                       *)
-(*       Canonical foo_unlockable := [unlockable fun foo].                    *)
-(*     This minimizes the comparison overhead for foo, while still allowing   *)
-(*     rewrite unlock to expose big_foo_expression.                           *)
-(* More information about these definitions and their use can be found in the *)
-(* ssreflect manual, and in specific comments below.                          *)
-(******************************************************************************)
+
+(**  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
+ advanced developers; in addition the following are defined:
+   #[#the str of v by f#]# == the Canonical s : str such that f s = v.
+        #[#the str of v#]# == the Canonical s : str that coerces to v.
+        argumentType c == the T such that c : forall x : T, P x.
+          returnType c == the R such that c : T -> R.
+     {type of c for s} == P s where c : forall x : T, P x.
+           phantom T v == singleton type with inhabitant Phantom T v.
+               phant T == singleton type with inhabitant Phant v.
+                 =^~ r == the converse of rewriting rule r (e.g., in a
+                          rewrite multirule).
+             unkeyed t == t, but treated as an unkeyed matching pattern by
+                          the ssreflect matching algorithm.
+             nosimpl t == t, but on the right-hand side of Definition C :=
+                          nosimpl disables expansion of C by /=.
+              locked t == t, but locked t is not convertible to t.
+       locked_with k t == t, but not convertible to t or locked_with k' t
+                          unless k = k' (with k : unit). Coq type-checking
+                          will be much more efficient if locked_with with a
+                          bespoke k is used for sealed definitions.
+          unlockable v == interface for sealed constant definitions of v.
+        Unlockable def == the unlockable that registers def : C = v.
+     #[#unlockable of C#]# == a clone for C of the canonical unlockable for the
+                          definition of C (e.g., if it uses locked_with).
+    #[#unlockable fun C#]# == #[#unlockable of C#]# with the expansion forced to be
+                          an explicit lambda expression.
+  -> The usage pattern for ADT operations is:
+       Definition foo_def x1 .. xn := big_foo_expression.
+       Fact foo_key : unit. Proof. by #[# #]#. Qed.
+       Definition foo := locked_with foo_key foo_def.
+       Canonical foo_unlockable := #[#unlockable fun foo#]#.
+     This minimizes the comparison overhead for foo, while still allowing
+     rewrite unlock to expose big_foo_expression.
+ More information about these definitions and their use can be found in the
+ ssreflect manual, and in specific comments below.                           **)
+
 
 
 Set Implicit Arguments.
@@ -62,15 +62,15 @@ Unset Printing Implicit Defensive.
 
 Module SsrSyntax.
 
-(* 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.   *)
+(**  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.    **)
 
 Reserved Notation "(* x 'is' y 'of' z 'isn't' // /= //= *)" (at level 8).
 Reserved Notation "(* 69 *)" (at level 69).
 
-(* Non ambiguous keyword to check if the SsrSyntax module is imported *)
+(**  Non ambiguous keyword to check if the SsrSyntax module is imported  **)
 Reserved Notation "(* Use to test if 'SsrSyntax_is_Imported' *)" (at level 8).
 
 Reserved Notation "<hidden n >" (at level 200).
@@ -81,10 +81,10 @@ End SsrSyntax.
 Export SsrMatchingSyntax.
 Export SsrSyntax.
 
-(* 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.                                       *)
+(**  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.                                        **)
 
 Declare Scope general_if_scope.
 Delimit Scope general_if_scope with GEN_IF.
@@ -102,7 +102,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,38 +118,38 @@ 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  *)
-(* 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:                   *)
-(*      [keyword ... ]                                                        *)
-(* Because the keyword follows a bracket it does not need to be reserved.     *)
-(* Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq *)
-(* Lists library) should be loaded before ssreflect so that their notations   *)
-(* do not mask all ssreflect forms.                                           *)
+(**  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:
+      #[#keyword ... #]#
+ Because the keyword follows a bracket it does not need to be reserved.
+ Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq
+ Lists library) should be loaded before ssreflect so that their notations
+ do not mask all ssreflect forms.                                            **)
 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    *)
-(* ":" 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       *)
-(* separate line rather than force-fit it at the right margin.                *)
+(**  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
+ separate line rather than force-fit it at the right margin.                 **)
 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         *)
-(* declarations. Note that (nat * nat : Type) is NOT equivalent to            *)
-(* (nat * nat)%type, whose inferred type is legacy type "Set".                *)
+(**  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".                 **)
 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.
 
-(* Constants for abstract: and [: name ] intro pattern *)
+(**  Constants for abstract: and #[#: name #]# intro pattern  **)
 Definition abstract_lock := unit.
 Definition abstract_key := tt.
 
@@ -163,31 +163,31 @@ Register abstract_lock as plugins.ssreflect.abstract_lock.
 Register abstract_key as plugins.ssreflect.abstract_key.
 Register abstract as plugins.ssreflect.abstract.
 
-(* Constants for tactic-views *)
+(**  Constants for tactic-views  **)
 Inductive external_view : Type := tactic_view of Type.
 
-(* 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         *)
-(*      proj_fun s = proj_val.                                                *)
-(* Typically proj_fun will be A record field accessors of struct_type, but    *)
-(* this need not be the case; it can be, for instance, a field of a record    *)
-(* type to which struct_type coerces; proj_val will likewise be coerced to    *)
-(* the return type of proj_fun. In all but the simplest cases, proj_fun       *)
-(* should be eta-expanded to allow for the insertion of implicit arguments.   *)
-(*   In the common case where proj_fun itself is a coercion, the "by" part    *)
-(* can be omitted entirely; in this case it is inferred by casting s to the   *)
-(* inferred type of proj_val. Obviously the latter can be fixed by using an   *)
-(* explicit cast on proj_val, and it is highly recommended to do so when the  *)
-(* return type intended for proj_fun is "Type", as the type inferred for      *)
-(* proj_val may vary because of sort polymorphism (it could be Set or Prop).  *)
-(*   Note when using the [the _ of _] form to generate a substructure from a  *)
-(* telescopes-style canonical hierarchy (implementing inheritance with        *)
-(* coercions), one should always project or coerce the value to the BASE      *)
-(* structure, because Coq will only find a Canonical derived structure for    *)
-(* the Canonical base structure -- not for a base structure that is specific  *)
-(* to proj_value.                                                             *)
+(**  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
+      proj_fun s = proj_val.
+ Typically proj_fun will be A record field accessors of struct_type, but
+ this need not be the case; it can be, for instance, a field of a record
+ type to which struct_type coerces; proj_val will likewise be coerced to
+ the return type of proj_fun. In all but the simplest cases, proj_fun
+ should be eta-expanded to allow for the insertion of implicit arguments.
+   In the common case where proj_fun itself is a coercion, the "by" part
+ can be omitted entirely; in this case it is inferred by casting s to the
+ inferred type of proj_val. Obviously the latter can be fixed by using an
+ explicit cast on proj_val, and it is highly recommended to do so when the
+ return type intended for proj_fun is "Type", as the type inferred for
+ proj_val may vary because of sort polymorphism (it could be Set or Prop).
+   Note when using the #[#the _ of _ #]# form to generate a substructure from a
+ telescopes-style canonical hierarchy (implementing inheritance with
+ coercions), one should always project or coerce the value to the BASE
+ structure, because Coq will only find a Canonical derived structure for
+ the Canonical base structure -- not for a base structure that is specific
+ to proj_value.                                                              **)
 
 Module TheCanonical.
 
@@ -210,11 +210,11 @@ 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 *)
-(* 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 *)
-(* hand side of the notations above.                                          *)
+(**  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
+ hand side of the notations above.                                           **)
 
 Notation "[ 'th' 'e' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _)
   (at level 0,  format "[ 'th' 'e'  sT  'of'  v  'by'  f ]") : form_scope.
@@ -222,37 +222,37 @@ 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
-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.               *)
-(* 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                             *)
-(*   Canonical a_type_struct := @Struct a_type ...                            *)
-(*   Definition my_type := a_type.                                            *)
-(* my_type doesn't effectively inherit the struct structure from a_type. Our  *)
-(* solution is to redeclare the instance as follows                           *)
-(*   Canonical my_type_struct := Eval hnf in [struct of my_type].             *)
-(* The special notation [str of _] must be defined for each Strucure "str"    *)
-(* with constructor "Str", typically as follows                               *)
-(*   Definition clone_str s :=                                                *)
-(*      let: Str _ x y ... z := s return {type of Str for s} -> str in        *)
-(*      fun k => k _ x y ... z.                                               *)
-(*    Notation "[ 'str' 'of' T 'for' s ]" := (@clone_str s (@Str T))          *)
-(*      (at level 0, format "[ 'str'  'of'  T  'for'  s ]") : form_scope.     *)
-(*    Notation "[ 'str' 'of' T ]" := (repack_str (fun x => @Str T x))         *)
-(*      (at level 0, format "[ 'str'  'of'  T ]") : form_scope.               *)
-(* The notation for the match return predicate is defined below; the eta      *)
-(* expansion in the second form serves both to distinguish it from the first  *)
-(* and to avoid the delta reduction problem.                                  *)
-(*   There are several variations on the notation and the definition of the   *)
-(* the "clone" function, for telescopes, mixin classes, and join (multiple    *)
-(* inheritance) classes. We describe a different idiom for clones in ssrfun;  *)
-(* it uses phantom types (see below) and static unification; see fintype and  *)
-(* ssralg for examples.                                                       *)
+(**  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.
+ 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
+   Canonical a_type_struct := @Struct a_type ...
+   Definition my_type := a_type.
+ my_type doesn't effectively inherit the struct structure from a_type. Our
+ solution is to redeclare the instance as follows
+   Canonical my_type_struct := Eval hnf in #[#struct of my_type#]#.
+ The special notation #[#str of _ #]# must be defined for each Strucure "str"
+ with constructor "Str", typically as follows
+   Definition clone_str s :=
+      let: Str _ x y ... z := s return {type of Str for s} -> str in
+      fun k => k _ x y ... z.
+    Notation " #[# 'str' 'of' T 'for' s #]#" := (@clone_str s (@Str T))
+      (at level 0, format " #[# 'str'  'of'  T  'for'  s #]#") : form_scope.
+    Notation " #[# 'str' 'of' T #]#" := (repack_str (fun x => @Str T x))
+      (at level 0, format " #[# 'str'  'of'  T #]#") : form_scope.
+ The notation for the match return predicate is defined below; the eta
+ expansion in the second form serves both to distinguish it from the first
+ and to avoid the delta reduction problem.
+   There are several variations on the notation and the definition of the
+ the "clone" function, for telescopes, mixin classes, and join (multiple
+ inheritance) classes. We describe a different idiom for clones in ssrfun;
+ it uses phantom types (see below) and static unification; see fintype and
+ ssralg for examples.                                                        **)
 
 Definition argumentType T P & forall x : T, P x := T.
 Definition dependentReturnType T P & forall x : T, P x := P.
@@ -261,81 +261,81 @@ 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). *)
-(* 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 *)
-(* (the latter interacts poorly with other Notation).                         *)
-(*   The definition of a (co)inductive type with a parameter p : p_type, that *)
-(* needs to use the operations of a structure                                 *)
-(*  Structure p_str : Type := p_Str {p_repr :> p_type; p_op : p_repr -> ...}  *)
-(* should be given as                                                         *)
-(*  Inductive indt_type (p : p_str) := Indt ... .                             *)
-(*  Definition indt_of (p : p_str) & phantom p_type p := indt_type p.         *)
-(*  Notation "{ 'indt' p }" := (indt_of (Phantom p)).                         *)
-(*  Definition indt p x y ... z : {indt p} := @Indt p x y ... z.              *)
-(*  Notation "[ 'indt' x y ... z ]" := (indt x y ... z).                      *)
-(* That is, the concrete type and its constructor should be shadowed by       *)
-(* definitions that use a phantom argument to infer and display the true      *)
-(* value of p (in practice, the "indt" constructor often performs additional  *)
-(* functions, like "locking" the representation -- see below).                *)
-(*   We also define a simpler version ("phant" / "Phant") of phantom for the  *)
-(* common case where p_type is Type.                                          *)
+(**  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
+ (the latter interacts poorly with other Notation).
+   The definition of a (co)inductive type with a parameter p : p_type, that
+ needs to use the operations of a structure
+  Structure p_str : Type := p_Str {p_repr :> p_type; p_op : p_repr -> ...}
+ should be given as
+  Inductive indt_type (p : p_str) := Indt ... .
+  Definition indt_of (p : p_str) & phantom p_type p := indt_type p.
+  Notation "{ 'indt' p }" := (indt_of (Phantom p)).
+  Definition indt p x y ... z : {indt p} := @Indt p x y ... z.
+  Notation " #[# 'indt' x y ... z #]#" := (indt x y ... z).
+ That is, the concrete type and its constructor should be shadowed by
+ definitions that use a phantom argument to infer and display the true
+ value of p (in practice, the "indt" constructor often performs additional
+ functions, like "locking" the representation -- see below).
+   We also define a simpler version ("phant" / "Phant") of phantom for the
+ common case where p_type is Type.                                           **)
 
 Variant phantom T (p : T) := Phantom.
 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:                               *)
-(*  - 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,   *)
-(*    to two arguments unifying with with a and b, repectively, regardless of *)
-(*    apparent head symbols.                                                  *)
-(*  - unkeyed x where x is a variable will match any subterm with the same    *)
-(*    type as x (when x would raise the 'indeterminate pattern' error).       *)
+(**  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,
+    to two arguments unifying with with a and b, repectively, regardless of
+    apparent head symbols.
+  - unkeyed x where x is a variable will match any subterm with the same
+    type as x (when x would raise the 'indeterminate pattern' error).        **)
 
 Notation unkeyed x := (let flex := x in flex).
 
-(* Ssreflect converse rewrite rule rule idiom. *)
+(**  Ssreflect converse rewrite rule rule idiom.  **)
 Definition ssr_converse R (r : R) := (Logic.I, r).
 Notation "=^~ r" := (ssr_converse r) (at level 100) : form_scope.
 
-(* 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   *)
-(*    Definition foo := nosimpl bar, foo (or foo t') will NOT be expanded by  *)
-(*    the /= and //= switches unless it is in a forcing context (e.g., in     *)
-(*    match foo t' with ... end, foo t' will be reduced if this allows the    *)
-(*    match to be reduced). Note that nosimpl bar is simply notation for a    *)
-(*    a term that beta-iota reduces to bar; hence rewrite /foo will replace   *)
-(*    foo by bar, and rewrite -/foo will replace bar by foo.                  *)
-(*    CAVEAT: nosimpl should not be used inside a Section, because the end of *)
-(*    section "cooking" removes the iota redex.                               *)
-(*  locked t is provably equal to t, but is not convertible to t; 'locked'    *)
-(*    provides support for selective rewriting, via the lock t : t = locked t *)
-(*    Lemma, and the ssreflect unlock tactic.                                 *)
-(*  locked_with k t is equal but not convertible to t, much like locked t,    *)
-(*    but supports explicit tagging with a value k : unit. This is used to    *)
-(*    mitigate a flaw in the term comparison heuristic of the Coq kernel,     *)
-(*    which treats all terms of the form locked t as equal and conpares their *)
-(*    arguments recursively, leading to an exponential blowup of comparison.  *)
-(*    For this reason locked_with should be used rather than locked when      *)
-(*    defining ADT operations. The unlock tactic does not support locked_with *)
-(*    but the unlock rewrite rule does, via the unlockable interface.         *)
-(*  we also use Module Type ascription to create truly opaque constants,      *)
-(*    because simple expansion of constants to reveal an unreducible term     *)
-(*    doubles the time complexity of a negative comparison. Such opaque       *)
-(*    constants can be expanded generically with the unlock rewrite rule.     *)
-(*    See the definition of card and subset in fintype for examples of this.  *)
+(**  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
+    Definition foo := nosimpl bar, foo (or foo t') will NOT be expanded by
+    the /= and //= switches unless it is in a forcing context (e.g., in
+    match foo t' with ... end, foo t' will be reduced if this allows the
+    match to be reduced). Note that nosimpl bar is simply notation for a
+    a term that beta-iota reduces to bar; hence rewrite /foo will replace
+    foo by bar, and rewrite -/foo will replace bar by foo.
+    CAVEAT: nosimpl should not be used inside a Section, because the end of
+    section "cooking" removes the iota redex.
+  locked t is provably equal to t, but is not convertible to t; 'locked'
+    provides support for selective rewriting, via the lock t : t = locked t
+    Lemma, and the ssreflect unlock tactic.
+  locked_with k t is equal but not convertible to t, much like locked t,
+    but supports explicit tagging with a value k : unit. This is used to
+    mitigate a flaw in the term comparison heuristic of the Coq kernel,
+    which treats all terms of the form locked t as equal and conpares their
+    arguments recursively, leading to an exponential blowup of comparison.
+    For this reason locked_with should be used rather than locked when
+    defining ADT operations. The unlock tactic does not support locked_with
+    but the unlock rewrite rule does, via the unlockable interface.
+  we also use Module Type ascription to create truly opaque constants,
+    because simple expansion of constants to reveal an unreducible term
+    doubles the time complexity of a negative comparison. Such opaque
+    constants can be expanded generically with the unlock rewrite rule.
+    See the definition of card and subset in fintype for examples of this.   **)
 
 Notation nosimpl t := (let: tt := tt in t).
 
@@ -347,11 +347,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]
@@ -359,7 +359,7 @@ Ltac done :=
    | case not_locked_false_eq_true; assumption
    | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
 
-(* Quicker done tactic not including split, syntax: /0/ *)
+(**  Quicker done tactic not including split, syntax: /0/  **)
 Ltac ssrdone0 :=
   trivial; hnf; intros; solve
    [ do ![solve [trivial | apply: sym_equal; trivial]
@@ -367,7 +367,7 @@ Ltac ssrdone0 :=
    | case not_locked_false_eq_true; assumption
    | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
 
-(* To unlock opaque constants. *)
+(**  To unlock opaque constants.  **)
 Structure unlockable T v := Unlockable {unlocked : T; _ : unlocked = v}.
 Lemma unlock T x C : @unlocked T x C = x. Proof. by case: C. Qed.
 
@@ -377,25 +377,25 @@ Notation "[ 'unlockable' 'of' C ]" := (@Unlockable _ _ C (unlock _))
 Notation "[ 'unlockable' 'fun' C ]" := (@Unlockable _ (fun _ => _) C (unlock _))
   (at level 0, format "[ 'unlockable'  'fun'  C ]") : form_scope.
 
-(* Generic keyed constant locking. *)
+(**  Generic keyed constant locking.  **)
 
-(* The argument order ensures that k is always compared before T. *)
+(**  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 *)
-(* below, but with caution as unkeyed matching can be expensive.              *)
+(**  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.
 
-(* Intensionaly, this instance will not apply to locked u. *)
+(**  Intensionaly, this instance will not apply to locked u.  **)
 Canonical locked_with_unlockable T k x :=
   @Unlockable T x (locked_with k x) (locked_withE k x).
 
-(* More accurate variant of unlock, and safer alternative to locked_withE. *)
+(**  More accurate variant of unlock, and safer alternative to locked_withE.  **)
 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 +416,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 +443,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,14 +461,14 @@ 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. *)
-(* Usage:                                                      *)
-(*   elim/abstract_context: (pattern) => G defG.               *)
-(*   vm_compute; rewrite {}defG {G}.                           *)
-(* Note that vm_cast are not stored in the proof term          *)
-(* for reductions occuring in the context, hence               *)
-(*   set here := pattern; vm_compute in (value of here)        *)
-(* blows up at Qed time.                                       *)
+(**  To focus non-ssreflect tactics on a subterm, eg vm_compute.
+ Usage:
+   elim/abstract_context: (pattern) => G defG.
+   vm_compute; rewrite {}defG {G}.
+ Note that vm_cast are not stored in the proof term
+ for reductions occuring in the context, hence
+   set here := pattern; vm_compute in (value of here)
+ blows up at Qed time.                                        **)
 Lemma abstract_context T (P : T -> Type) x :
   (forall Q, Q = P -> Q x) -> P x.
 Proof. by move=> /(_ P); apply. Qed.
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index 99ff943e61..70be97feec 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -12,205 +12,205 @@
 
 Require Import ssreflect.
 
-(******************************************************************************)
-(* This file contains the basic definitions and notations for working with    *)
-(* functions. The definitions provide for:                                    *)
-(*                                                                            *)
-(* - Pair projections:                                                        *)
-(*    p.1  == first element of a pair                                         *)
-(*    p.2  == second element of a pair                                        *)
-(*   These notations also apply to p : P /\ Q, via an and >-> pair coercion.  *)
-(*                                                                            *)
-(* - Simplifying functions, beta-reduced by /= and simpl:                     *)
-(*           [fun : T => E] == constant function from type T that returns E   *)
-(*             [fun x => E] == unary function                                 *)
-(*         [fun x : T => E] == unary function with explicit domain type       *)
-(*           [fun x y => E] == binary function                                *)
-(*       [fun x y : T => E] == binary function with common domain type        *)
-(*         [fun (x : T) y => E] \                                             *)
-(* [fun (x : xT) (y : yT) => E] | == binary function with (some) explicit,    *)
-(*         [fun x (y : T) => E] / independent domain types for each argument  *)
-(*                                                                            *)
-(* - Partial functions using option type:                                     *)
-(*     oapp f d ox == if ox is Some x returns f x,        d otherwise         *)
-(*      odflt d ox == if ox is Some x returns x,          d otherwise         *)
-(*      obind f ox == if ox is Some x returns f x,        None otherwise      *)
-(*       omap f ox == if ox is Some x returns Some (f x), None otherwise      *)
-(*                                                                            *)
-(* - Singleton types:                                                         *)
-(*  all_equal_to x0 == x0 is the only value in its type, so any such value    *)
-(*                     can be rewritten to x0.                                *)
-(*                                                                            *)
-(* - A generic wrapper type:                                                  *)
-(*       wrapped T == the inductive type with values Wrap x for x : T.        *)
-(*        unwrap w == the projection of w : wrapped T on T.                   *)
-(*          wrap x == the canonical injection of x : T into wrapped T; it is  *)
-(*                    equivalent to Wrap x, but is declared as a (default)    *)
-(*                    Canonical Structure, which lets the Coq HO unification  *)
-(*                    automatically expand x into unwrap (wrap x). The delta  *)
-(*                    reduction of wrap x to Wrap can be exploited to         *)
-(*                    introduce controlled nondeterminism in Canonical        *)
-(*                    Structure inference, as in the implementation of        *)
-(*                    the mxdirect predicate in matrix.v.                     *)
-(*                                                                            *)
-(* - Sigma types:                                                             *)
-(*           tag w == the i of w : {i : I & T i}.                             *)
-(*        tagged w == the T i component of w : {i : I & T i}.                 *)
-(*      Tagged T x == the {i : I & T i} with component x : T i.               *)
-(*          tag2 w == the i of w : {i : I & T i & U i}.                       *)
-(*       tagged2 w == the T i component of w : {i : I & T i & U i}.           *)
-(*      tagged2' w == the U i component of w : {i : I & T i & U i}.           *)
-(* Tagged2 T U x y == the {i : I & T i} with components x : T i and y : U i.  *)
-(*          sval u == the x of u : {x : T | P x}.                             *)
-(*         s2val u == the x of u : {x : T | P x & Q x}.                       *)
-(*   The properties of sval u, s2val u are given by lemmas svalP, s2valP, and *)
-(*   s2valP'. We provide coercions sigT2 >-> sigT and sig2 >-> sig >-> sigT.  *)
-(*   A suite of lemmas (all_sig, ...) let us skolemize sig, sig2, sigT, sigT2 *)
-(*   and pair, e.g.,                                                          *)
-(*     have /all_sig[f fP] (x : T): {y : U | P y} by ...                      *)
-(*   yields an f : T -> U such that fP : forall x, P (f x).                   *)
-(* - Identity functions:                                                      *)
-(*    id           == NOTATION for the explicit identity function fun x => x. *)
-(*    @id T        == notation for the explicit identity at type T.           *)
-(*    idfun        == an expression with a head constant, convertible to id;  *)
-(*                    idfun x simplifies to x.                                *)
-(*    @idfun T     == the expression above, specialized to type T.            *)
-(*    phant_id x y == the function type phantom _ x -> phantom _ y.           *)
-(* *** In addition to their casual use in functional programming, identity    *)
-(* functions are often used to trigger static unification as part of the      *)
-(* construction of dependent Records and Structures. For example, if we need  *)
-(* a structure sT over a type T, we take as arguments T, sT, and a "dummy"    *)
-(* function T -> sort sT:                                                     *)
-(*   Definition foo T sT & T -> sort sT := ...                                *)
-(* We can avoid specifying sT directly by calling foo (@id T), or specify     *)
-(* the call completely while still ensuring the consistency of T and sT, by   *)
-(* calling @foo T sT idfun. The phant_id type allows us to extend this trick  *)
-(* to non-Type canonical projections. It also allows us to sidestep           *)
-(* dependent type constraints when building explicit records, e.g., given     *)
-(*    Record r := R {x; y : T(x)}.                                            *)
-(* if we need to build an r from a given y0 while inferring some x0, such     *)
-(* that y0 : T(x0), we pose                                                   *)
-(*    Definition mk_r .. y .. (x := ...) y' & phant_id y y' := R x y'.        *)
-(* Calling @mk_r .. y0 .. id will cause Coq to use y' := y0, while checking   *)
-(* the dependent type constraint y0 : T(x0).                                  *)
-(*                                                                            *)
-(* - Extensional equality for functions and relations (i.e. functions of two  *)
-(*   arguments):                                                              *)
-(*    f1 =1 f2      ==  f1 x is equal to f2 x for all x.                      *)
-(*    f1 =1 f2 :> A ==    ... and f2 is explicitly typed.                     *)
-(*    f1 =2 f2      ==  f1 x y is equal to f2 x y for all x y.                *)
-(*    f1 =2 f2 :> A ==    ... and f2 is explicitly typed.                     *)
-(*                                                                            *)
-(* - Composition for total and partial functions:                             *)
-(*            f^~ y == function f with second argument specialised to y,      *)
-(*                     i.e., fun x => f x y                                   *)
-(*                     CAVEAT: conditional (non-maximal) implicit arguments   *)
-(*                     of f are NOT inserted in this context                  *)
-(*            @^~ x == application at x, i.e., fun f => f x                   *)
-(*          [eta f] == the explicit eta-expansion of f, i.e., fun x => f x    *)
-(*                     CAVEAT: conditional (non-maximal) implicit arguments   *)
-(*                     of f are NOT inserted in this context.                 *)
-(*          fun=> v := the constant function fun _ => v.                      *)
-(*        f1 \o f2  == composition of f1 and f2.                              *)
-(*                     Note: (f1 \o f2) x simplifies to f1 (f2 x).            *)
-(*         f1 \; f2 == categorical composition of f1 and f2. This expands to  *)
-(*                     to f2 \o f1 and (f1 \; f2) x simplifies to f2 (f1 x).  *)
-(*      pcomp f1 f2 == composition of partial functions f1 and f2.            *)
-(*                                                                            *)
-(*                                                                            *)
-(* - Properties of functions:                                                 *)
-(*      injective f <-> f is injective.                                       *)
-(*       cancel f g <-> g is a left inverse of f / f is a right inverse of g. *)
-(*      pcancel f g <-> g is a left inverse of f where g is partial.          *)
-(*      ocancel f g <-> g is a left inverse of f where f is partial.          *)
-(*      bijective f <-> f is bijective (has a left and right inverse).        *)
-(*     involutive f <-> f is involutive.                                      *)
-(*                                                                            *)
-(* - Properties for operations.                                               *)
-(*              left_id e op <-> e is a left identity for op (e op x = x).    *)
-(*             right_id e op <-> e is a right identity for op (x op e = x).   *)
-(*     left_inverse e inv op <-> inv is a left inverse for op wrt identity e, *)
-(*                               i.e., (inv x) op x = e.                      *)
-(*    right_inverse e inv op <-> inv is a right inverse for op wrt identity e *)
-(*                               i.e., x op (i x) = e.                        *)
-(*         self_inverse e op <-> each x is its own op-inverse (x op x = e).   *)
-(*             idempotent op <-> op is idempotent for op (x op x = x).        *)
-(*              associative op <-> op is associative, i.e.,                   *)
-(*                               x op (y op z) = (x op y) op z.               *)
-(*            commutative op <-> op is commutative (x op y = y op x).         *)
-(*       left_commutative op <-> op is left commutative, i.e.,                *)
-(*                                   x op (y op z) = y op (x op z).           *)
-(*      right_commutative op <-> op is right commutative, i.e.,               *)
-(*                                   (x op y) op z = (x op z) op y.           *)
-(*            left_zero z op <-> z is a left zero for op (z op x = z).        *)
-(*           right_zero z op <-> z is a right zero for op (x op z = z).       *)
-(*  left_distributive op1 op2 <-> op1 distributes over op2 to the left:       *)
-(*                             (x op2 y) op1 z = (x op1 z) op2 (y op1 z).     *)
-(* right_distributive op1 op2 <-> op distributes over add to the right:       *)
-(*                             x op1 (y op2 z) = (x op1 z) op2 (x op1 z).     *)
-(*        interchange op1 op2 <-> op1 and op2 satisfy an interchange law:     *)
-(*                        (x op2 y) op1 (z op2 t) = (x op1 z) op2 (y op1 t).  *)
-(*  Note that interchange op op is a commutativity property.                  *)
-(*         left_injective op <-> op is injective in its left argument:        *)
-(*                             x op y = z op y -> x = z.                      *)
-(*        right_injective op <-> op is injective in its right argument:       *)
-(*                             x op y = x op z -> y = z.                      *)
-(*          left_loop inv op <-> op, inv obey the inverse loop left axiom:    *)
-(*                              (inv x) op (x op y) = y for all x, y, i.e.,   *)
-(*                              op (inv x) is always a left inverse of op x   *)
-(*      rev_left_loop inv op <-> op, inv obey the inverse loop reverse left   *)
-(*                              axiom: x op ((inv x) op y) = y, for all x, y. *)
-(*         right_loop inv op <-> op, inv obey the inverse loop right axiom:   *)
-(*                              (x op y) op (inv y) = x for all x, y.         *)
-(*     rev_right_loop inv op <-> op, inv obey the inverse loop reverse right  *)
-(*                              axiom: (x op y) op (inv y) = x for all x, y.  *)
-(*   Note that familiar "cancellation" identities like x + y - y = x or       *)
-(* x - y + y = x are respectively instances of right_loop and rev_right_loop  *)
-(* The corresponding lemmas will use the K and NK/VK suffixes, respectively.  *)
-(*                                                                            *)
-(* - Morphisms for functions and relations:                                   *)
-(*    {morph f : x / a >-> r} <-> f is a morphism with respect to functions   *)
-(*                               (fun x => a) and (fun x => r); if r == R[x], *)
-(*                               this states that f a = R[f x] for all x.     *)
-(*          {morph f : x / a} <-> f is a morphism with respect to the         *)
-(*                               function expression (fun x => a). This is    *)
-(*                               shorthand for {morph f : x / a >-> a}; note  *)
-(*                               that the two instances of a are often        *)
-(*                               interpreted at different types.              *)
-(*  {morph f : x y / a >-> r} <-> f is a morphism with respect to functions   *)
-(*                               (fun x y => a) and (fun x y => r).           *)
-(*        {morph f : x y / a} <-> f is a morphism with respect to the         *)
-(*                               function expression (fun x y => a).          *)
-(*     {homo f : x / a >-> r} <-> f is a homomorphism with respect to the     *)
-(*                               predicates (fun x => a) and (fun x => r);    *)
-(*                               if r == R[x], this states that a -> R[f x]   *)
-(*                               for all x.                                   *)
-(*           {homo f : x / a} <-> f is a homomorphism with respect to the     *)
-(*                               predicate expression (fun x => a).           *)
-(*   {homo f : x y / a >-> r} <-> f is a homomorphism with respect to the     *)
-(*                               relations (fun x y => a) and (fun x y => r). *)
-(*         {homo f : x y / a} <-> f is a homomorphism with respect to the     *)
-(*                               relation expression (fun x y => a).          *)
-(*     {mono f : x / a >-> r} <-> f is monotone with respect to projectors    *)
-(*                               (fun x => a) and (fun x => r); if r == R[x], *)
-(*                               this states that R[f x] = a for all x.       *)
-(*           {mono f : x / a} <-> f is monotone with respect to the projector *)
-(*                               expression (fun x => a).                     *)
-(*   {mono f : x y / a >-> r} <-> f is monotone with respect to relators      *)
-(*                               (fun x y => a) and (fun x y => r).           *)
-(*         {mono f : x y / a} <-> f is monotone with respect to the relator   *)
-(*                               expression (fun x y => a).                   *)
-(*                                                                            *)
-(* The file also contains some basic lemmas for the above concepts.           *)
-(* Lemmas relative to cancellation laws use some abbreviated suffixes:        *)
-(*   K - a cancellation rule like esymK : cancel (@esym T x y) (@esym T y x). *)
-(*  LR - a lemma moving an operation from the left hand side of a relation to *)
-(*       the right hand side, like canLR: cancel g f -> x = g y -> f x = y.   *)
-(*  RL - a lemma moving an operation from the right to the left, e.g., canRL. *)
-(* Beware that the LR and RL orientations refer to an "apply" (back chaining) *)
-(* usage; when using the same lemmas with "have" or "move" (forward chaining) *)
-(* the directions will be reversed!.                                          *)
-(******************************************************************************)
+
+(**  This file contains the basic definitions and notations for working with
+ functions. The definitions provide for:
+
+ - Pair projections:
+    p.1  == first element of a pair
+    p.2  == second element of a pair
+   These notations also apply to p : P /\ Q, via an and >-> pair coercion.
+
+ - Simplifying functions, beta-reduced by /= and simpl:
+           #[#fun : T => E#]# == constant function from type T that returns E
+             #[#fun x => E#]# == unary function
+         #[#fun x : T => E#]# == unary function with explicit domain type
+           #[#fun x y => E#]# == binary function
+       #[#fun x y : T => E#]# == binary function with common domain type
+         #[#fun (x : T) y => E#]# \
+ #[#fun (x : xT) (y : yT) => E#]# | == binary function with (some) explicit,
+         #[#fun x (y : T) => E#]# / independent domain types for each argument
+
+ - Partial functions using option type:
+     oapp f d ox == if ox is Some x returns f x,        d otherwise
+      odflt d ox == if ox is Some x returns x,          d otherwise
+      obind f ox == if ox is Some x returns f x,        None otherwise
+       omap f ox == if ox is Some x returns Some (f x), None otherwise
+
+ - Singleton types:
+  all_equal_to x0 == x0 is the only value in its type, so any such value
+                     can be rewritten to x0.
+
+ - A generic wrapper type:
+       wrapped T == the inductive type with values Wrap x for x : T.
+        unwrap w == the projection of w : wrapped T on T.
+          wrap x == the canonical injection of x : T into wrapped T; it is
+                    equivalent to Wrap x, but is declared as a (default)
+                    Canonical Structure, which lets the Coq HO unification
+                    automatically expand x into unwrap (wrap x). The delta
+                    reduction of wrap x to Wrap can be exploited to
+                    introduce controlled nondeterminism in Canonical
+                    Structure inference, as in the implementation of
+                    the mxdirect predicate in matrix.v.
+
+ - Sigma types:
+           tag w == the i of w : {i : I & T i}.
+        tagged w == the T i component of w : {i : I & T i}.
+      Tagged T x == the {i : I & T i} with component x : T i.
+          tag2 w == the i of w : {i : I & T i & U i}.
+       tagged2 w == the T i component of w : {i : I & T i & U i}.
+      tagged2' w == the U i component of w : {i : I & T i & U i}.
+ Tagged2 T U x y == the {i : I & T i} with components x : T i and y : U i.
+          sval u == the x of u : {x : T | P x}.
+         s2val u == the x of u : {x : T | P x & Q x}.
+   The properties of sval u, s2val u are given by lemmas svalP, s2valP, and
+   s2valP'. We provide coercions sigT2 >-> sigT and sig2 >-> sig >-> sigT.
+   A suite of lemmas (all_sig, ...) let us skolemize sig, sig2, sigT, sigT2
+   and pair, e.g.,
+     have /all_sig#[#f fP#]# (x : T): {y : U | P y} by ...
+   yields an f : T -> U such that fP : forall x, P (f x).
+ - Identity functions:
+    id           == NOTATION for the explicit identity function fun x => x.
+    @id T        == notation for the explicit identity at type T.
+    idfun        == an expression with a head constant, convertible to id;
+                    idfun x simplifies to x.
+    @idfun T     == the expression above, specialized to type T.
+    phant_id x y == the function type phantom _ x -> phantom _ y.
+ *** In addition to their casual use in functional programming, identity
+ functions are often used to trigger static unification as part of the
+ construction of dependent Records and Structures. For example, if we need
+ a structure sT over a type T, we take as arguments T, sT, and a "dummy"
+ function T -> sort sT:
+   Definition foo T sT & T -> sort sT := ...
+ We can avoid specifying sT directly by calling foo (@id T), or specify
+ the call completely while still ensuring the consistency of T and sT, by
+ calling @foo T sT idfun. The phant_id type allows us to extend this trick
+ to non-Type canonical projections. It also allows us to sidestep
+ dependent type constraints when building explicit records, e.g., given
+    Record r := R {x; y : T(x)}.
+ if we need to build an r from a given y0 while inferring some x0, such
+ that y0 : T(x0), we pose
+    Definition mk_r .. y .. (x := ...) y' & phant_id y y' := R x y'.
+ Calling @mk_r .. y0 .. id will cause Coq to use y' := y0, while checking
+ the dependent type constraint y0 : T(x0).
+
+ - Extensional equality for functions and relations (i.e. functions of two
+   arguments):
+    f1 =1 f2      ==  f1 x is equal to f2 x for all x.
+    f1 =1 f2 :> A ==    ... and f2 is explicitly typed.
+    f1 =2 f2      ==  f1 x y is equal to f2 x y for all x y.
+    f1 =2 f2 :> A ==    ... and f2 is explicitly typed.
+
+ - Composition for total and partial functions:
+            f^~ y == function f with second argument specialised to y,
+                     i.e., fun x => f x y
+                     CAVEAT: conditional (non-maximal) implicit arguments
+                     of f are NOT inserted in this context
+            @^~ x == application at x, i.e., fun f => f x
+          #[#eta f#]# == the explicit eta-expansion of f, i.e., fun x => f x
+                     CAVEAT: conditional (non-maximal) implicit arguments
+                     of f are NOT inserted in this context.
+          fun=> v := the constant function fun _ => v.
+        f1 \o f2  == composition of f1 and f2.
+                     Note: (f1 \o f2) x simplifies to f1 (f2 x).
+         f1 \; f2 == categorical composition of f1 and f2. This expands to
+                     to f2 \o f1 and (f1 \; f2) x simplifies to f2 (f1 x).
+      pcomp f1 f2 == composition of partial functions f1 and f2.
+
+
+ - Properties of functions:
+      injective f <-> f is injective.
+       cancel f g <-> g is a left inverse of f / f is a right inverse of g.
+      pcancel f g <-> g is a left inverse of f where g is partial.
+      ocancel f g <-> g is a left inverse of f where f is partial.
+      bijective f <-> f is bijective (has a left and right inverse).
+     involutive f <-> f is involutive.
+
+ - Properties for operations.
+              left_id e op <-> e is a left identity for op (e op x = x).
+             right_id e op <-> e is a right identity for op (x op e = x).
+     left_inverse e inv op <-> inv is a left inverse for op wrt identity e,
+                               i.e., (inv x) op x = e.
+    right_inverse e inv op <-> inv is a right inverse for op wrt identity e
+                               i.e., x op (i x) = e.
+         self_inverse e op <-> each x is its own op-inverse (x op x = e).
+             idempotent op <-> op is idempotent for op (x op x = x).
+              associative op <-> op is associative, i.e.,
+                               x op (y op z) = (x op y) op z.
+            commutative op <-> op is commutative (x op y = y op x).
+       left_commutative op <-> op is left commutative, i.e.,
+                                   x op (y op z) = y op (x op z).
+      right_commutative op <-> op is right commutative, i.e.,
+                                   (x op y) op z = (x op z) op y.
+            left_zero z op <-> z is a left zero for op (z op x = z).
+           right_zero z op <-> z is a right zero for op (x op z = z).
+  left_distributive op1 op2 <-> op1 distributes over op2 to the left:
+                             (x op2 y) op1 z = (x op1 z) op2 (y op1 z).
+ right_distributive op1 op2 <-> op distributes over add to the right:
+                             x op1 (y op2 z) = (x op1 z) op2 (x op1 z).
+        interchange op1 op2 <-> op1 and op2 satisfy an interchange law:
+                        (x op2 y) op1 (z op2 t) = (x op1 z) op2 (y op1 t).
+  Note that interchange op op is a commutativity property.
+         left_injective op <-> op is injective in its left argument:
+                             x op y = z op y -> x = z.
+        right_injective op <-> op is injective in its right argument:
+                             x op y = x op z -> y = z.
+          left_loop inv op <-> op, inv obey the inverse loop left axiom:
+                              (inv x) op (x op y) = y for all x, y, i.e.,
+                              op (inv x) is always a left inverse of op x
+      rev_left_loop inv op <-> op, inv obey the inverse loop reverse left
+                              axiom: x op ((inv x) op y) = y, for all x, y.
+         right_loop inv op <-> op, inv obey the inverse loop right axiom:
+                              (x op y) op (inv y) = x for all x, y.
+     rev_right_loop inv op <-> op, inv obey the inverse loop reverse right
+                              axiom: (x op y) op (inv y) = x for all x, y.
+   Note that familiar "cancellation" identities like x + y - y = x or
+ x - y + y = x are respectively instances of right_loop and rev_right_loop
+ The corresponding lemmas will use the K and NK/VK suffixes, respectively.
+
+ - Morphisms for functions and relations:
+    {morph f : x / a >-> r} <-> f is a morphism with respect to functions
+                               (fun x => a) and (fun x => r); if r == R#[#x#]#,
+                               this states that f a = R#[#f x#]# for all x.
+          {morph f : x / a} <-> f is a morphism with respect to the
+                               function expression (fun x => a). This is
+                               shorthand for {morph f : x / a >-> a}; note
+                               that the two instances of a are often
+                               interpreted at different types.
+  {morph f : x y / a >-> r} <-> f is a morphism with respect to functions
+                               (fun x y => a) and (fun x y => r).
+        {morph f : x y / a} <-> f is a morphism with respect to the
+                               function expression (fun x y => a).
+     {homo f : x / a >-> r} <-> f is a homomorphism with respect to the
+                               predicates (fun x => a) and (fun x => r);
+                               if r == R#[#x#]#, this states that a -> R#[#f x#]#
+                               for all x.
+           {homo f : x / a} <-> f is a homomorphism with respect to the
+                               predicate expression (fun x => a).
+   {homo f : x y / a >-> r} <-> f is a homomorphism with respect to the
+                               relations (fun x y => a) and (fun x y => r).
+         {homo f : x y / a} <-> f is a homomorphism with respect to the
+                               relation expression (fun x y => a).
+     {mono f : x / a >-> r} <-> f is monotone with respect to projectors
+                               (fun x => a) and (fun x => r); if r == R#[#x#]#,
+                               this states that R#[#f x#]# = a for all x.
+           {mono f : x / a} <-> f is monotone with respect to the projector
+                               expression (fun x => a).
+   {mono f : x y / a >-> r} <-> f is monotone with respect to relators
+                               (fun x y => a) and (fun x y => r).
+         {mono f : x y / a} <-> f is monotone with respect to the relator
+                               expression (fun x y => a).
+
+ The file also contains some basic lemmas for the above concepts.
+ Lemmas relative to cancellation laws use some abbreviated suffixes:
+   K - a cancellation rule like esymK : cancel (@esym T x y) (@esym T y x).
+  LR - a lemma moving an operation from the left hand side of a relation to
+       the right hand side, like canLR: cancel g f -> x = g y -> f x = y.
+  RL - a lemma moving an operation from the right to the left, e.g., canRL.
+ Beware that the LR and RL orientations refer to an "apply" (back chaining)
+ usage; when using the same lemmas with "have" or "move" (forward chaining)
+ the directions will be reversed!.                                           **)
+
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -220,7 +220,7 @@ Declare Scope fun_scope.
 Delimit Scope fun_scope with FUN.
 Open Scope fun_scope.
 
-(* Notations for argument transpose *)
+(**  Notations for argument transpose  **)
 Notation "f ^~ y" := (fun x => f x y)
   (at level 10, y at level 8, no associativity, format "f ^~  y") : fun_scope.
 Notation "@^~ x" := (fun f => f x)
@@ -230,7 +230,7 @@ Declare Scope pair_scope.
 Delimit Scope pair_scope with PAIR.
 Open Scope pair_scope.
 
-(* Notations for pair/conjunction projections *)
+(**  Notations for pair/conjunction projections  **)
 Notation "p .1" := (fst p)
   (at level 2, left associativity, format "p .1") : pair_scope.
 Notation "p .2" := (snd p)
@@ -241,8 +241,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  *)
-(* encode partial functions.                                  *)
+(**  Complements on the option type constructor, used below to
+ encode partial functions.                                   **)
 
 Module Option.
 
@@ -262,7 +262,7 @@ Notation obind := Option.bind.
 Notation omap := Option.map.
 Notation some := (@Some _) (only parsing).
 
-(* Shorthand for some basic equality lemmas. *)
+(**  Shorthand for some basic equality lemmas.  **)
 
 Notation erefl := refl_equal.
 Notation ecast i T e x := (let: erefl in _ = i := e return T in x).
@@ -271,31 +271,31 @@ Definition nesym := sym_not_eq.
 Definition etrans := trans_eq.
 Definition congr1 := f_equal.
 Definition congr2 := f_equal2.
-(* Force at least one implicit when used as a view. *)
+(**  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.
 
-(* A generic wrapper type *)
+(**  A generic wrapper type  **)
 
 Structure wrapped T := Wrap {unwrap : T}.
 Canonical wrap T x := @Wrap T x.
 
 Prenex Implicits unwrap wrap Wrap.
 
-(* Syntax for defining auxiliary recursive function.          *)
-(*  Usage:                                                    *)
-(* Section FooDefinition.                                     *)
-(* Variables (g1 : T1) (g2 : T2).  (globals)                  *)
-(* Fixoint foo_auxiliary (a3 : T3) ... :=                     *)
-(*        body, using [rec e3, ...] for recursive calls       *)
-(* where "[ 'rec' a3 , a4 , ... ]" := foo_auxiliary.          *)
-(* Definition foo x y .. := [rec e1, ...].                    *)
-(* + proofs about foo                                         *)
-(* End FooDefinition.                                         *)
+(**  Syntax for defining auxiliary recursive function.
+  Usage:
+ Section FooDefinition.
+ Variables (g1 : T1) (g2 : T2).  (globals)
+ Fixoint foo_auxiliary (a3 : T3) ... :=
+        body, using #[#rec e3, ... #]# for recursive calls
+ where " #[# 'rec' a3 , a4 , ... #]#" := foo_auxiliary.
+ Definition foo x y .. := #[#rec e1, ... #]#.
+ + proofs about foo
+ End FooDefinition.                                          **)
 
 Reserved Notation "[ 'rec' a0 ]"
   (at level 0, format "[ 'rec'  a0 ]").
@@ -321,8 +321,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,     *)
-(* i.e., which simpl and /= beta expand (this is complementary to nosimpl). *)
+(**  Definitions and notation for explicit functions with simplification,
+ i.e., which simpl and /= beta expand (this is complementary to nosimpl).  **)
 
 Section SimplFun.
 
@@ -364,11 +364,11 @@ Notation "[ 'fun' ( x : xT ) ( y : yT ) => E ]" :=
     (fun x : xT => [fun y : yT => E])
   (at level 0, x ident, y ident, only parsing) : fun_scope.
 
-(* For delta functions in eqtype.v. *)
+(**  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  *)
-(* sugar.                                                                     *)
+(**  Extensional equality, for unary and binary functions, including syntactic
+ sugar.                                                                      **)
 
 Section ExtensionalEquality.
 
@@ -441,7 +441,7 @@ Notation "@ 'idfun' T " := (@id_head T explicit_id_key)
 
 Definition phant_id T1 T2 v1 v2 := phantom T1 v1 -> phantom T2 v2.
 
-(* Strong sigma types. *)
+(**  Strong sigma types.  **)
 
 Section Tag.
 
@@ -475,9 +475,9 @@ Lemma all_tag2 I T U V :
   {f : forall i, T i & forall i, U i (f i) & forall i, V i (f i)}.
 Proof. by case/all_tag=> f /all_pair[]; exists f. Qed.
 
-(* Refinement types. *)
+(**  Refinement types.  **)
 
-(* Prenex Implicits and renaming. *)
+(**  Prenex Implicits and renaming.  **)
 Notation sval := (@proj1_sig _ _).
 Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'").
 
@@ -516,16 +516,16 @@ Section Morphism.
 
 Variables (aT rT sT : Type) (f : aT -> rT).
 
-(* Morphism property for unary and binary functions *)
+(**  Morphism property for unary and binary functions  **)
 Definition morphism_1 aF rF := forall x, f (aF x) = rF (f x).
 Definition morphism_2 aOp rOp := forall x y, f (aOp x y) = rOp (f x) (f y).
 
-(* Homomorphism property for unary and binary relations *)
+(**  Homomorphism property for unary and binary relations  **)
 Definition homomorphism_1 (aP rP : _ -> Prop) := forall x, aP x -> rP (f x).
 Definition homomorphism_2 (aR rR : _ -> _ -> Prop) :=
   forall x y, aR x y -> rR (f x) (f y).
 
-(* Stability property for unary and binary relations *)
+(**  Stability property for unary and binary relations  **)
 Definition monomorphism_1 (aP rP : _ -> sT) := forall x, rP (f x) = aP x.
 Definition monomorphism_2 (aR rR : _ -> _ -> sT) :=
   forall x y, rR (f x) (f y) = aR x y.
@@ -602,16 +602,16 @@ 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     *)
-(* 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   *)
-(* partial function.                                                         *)
+(**  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
+ partial function.                                                          **)
 
 Section Injections.
 
-(* 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). *)
+(**  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).
 
 Definition injective := forall x1 x2, f x1 = f x2 -> x1 = x2.
@@ -641,10 +641,10 @@ End Injections.
 
 Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed.
 
-(* Force implicits to use as a view. *)
+(**  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.