Make an appropriate use of the order library everywhere (#278, #280, #282, #283, #285, #286, #288, #296, #330, #334, and #341)

ssrnum related changes:
- Redefine the intermediate structure between `idomainType` and `numDomainType`,
  which is `normedDomainType` (normed integral domain without an order).
- Generalize (by using `normedDomainType` or the order structures), relocate
  (to order.v), and rename ssrnum related definitions and lemmas.
- Add a compatibility module `Num.mc_1_9` and export it to check compilation.
- Remove the use of the deprecated definitions and lemmas from entire theories.
- Implement factories mechanism to construct several ordered and num structures
  from fewer axioms.

order related changes:
- Reorganize the hierarchy of finite lattice structures. Finite lattices have
  top and bottom elements except for empty set. Therefore we removed finite
  lattice structures without top and bottom.
- Reorganize the theory modules in order.v:
  + `LTheory` (lattice and partial order, without complement and totality)
  + `CTheory` (`LTheory` + complement)
  + `Theory` (all)
- Give a unique head symbol for `Total.mixin_of`.
- Replace reverse and `^r` with converse and `^c` respectively.
- Fix packing and cloning functions and notations.
- Provide more ordered type instances:
  Products and lists can be ordered in two different ways: the lexicographical
  ordering and the pointwise ordering. Now their canonical instances are not
  exported to make the users choose them.
- Export `Order.*.Exports` modules by default.
- Specify the core hint database explicitly in order.v. (see #252)
- Apply 80 chars per line restriction.

General changes:
- Give consistency to shape of formulae and namings of `lt_def` and `lt_neqAle`
  like lemmas:
  lt_def    x y : (x < y) = (y != x) && (x <= y),
  lt_neqAle x y : (x < y) = (x != y) && (x <= y).
- Enable notation overloading by using scopes and displays:
  + Define `min` and `max` notations (`minr` and `maxr` for `ring_display`) as
    aliases of `meet` and `join` specialized for `total_display`.
  + Provide the `ring_display` version of `le`, `lt`, `ge`, `gt`, `leif`, and
    `comparable` notations and their explicit variants in `Num.Def`.
  + Define 3 variants of `[arg min_(i < n | P) F]` and `[arg max_(i < n | P) F]`
    notations in `nat_scope` (specialized for nat), `order_scope` (general
    version), and `ring_scope` (specialized for `ring_display`).
- Update documents and put CHANGELOG entries.

0 files changed, 0 insertions, 0 deletions