- Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull`
  (`#9984 <https://github.com/coq/coq/pull/9984>`_,
  by Jean-Christophe Léchenet and Oliver Nash).