update changelog and documentation

[affeldt-aist]

with the following structures added to order_topology.v by PR #1810

HB.structure Definition POrderedNbhs d :=
  { T of Nbhs T & Order.isPOrder d T }.

HB.structure Definition POrderedTopological d :=
  { T of Topological T & Order.isPOrder d T }.

HB.structure Definition POrderedUniform d :=
  {T of Uniform T & Order.isPOrder d T}.

HB.structure Definition POrderedPseudoMetric d (R : numDomainType) :=
  {T of PseudoMetric R T & Order.isPOrder d T}.

HB.structure Definition POrderedPointedTopological d :=
  {T of PointedTopological T & Order.isPOrder d T}.