measurable types are not pointed by default any more

[affeldt-aist]

Motivation for this change

fixes #796

fyi: @shinya-katsumata @CohenCyril

We would like this change to be reflected in master as soon as possible so as to be able to work
with the following definition:

Structure distr := Distr {
  mu :> T -> R ;
  _  :  forall x, 0 <= mu x ;
  _  :  summable [set: T] (EFin \o mu) ;
  _  :  \int[@counting (discrete_measurable_space T) R]_x (mu x) <= 1
}.

without requiring T to be a pointedType, only a choiceType,
to preserve the generality of distr from the experimental_reals package
@strub @lyonel2017 (just substituting summable and psum from their
MathComp-Analysis equivalent to use the library more easily).

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels