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

[affeldt-aist]

The patch we merged to MathComp, i.e., the addition of the following
between Module Import Ring. and End Ring. in ssralg.v:

HB.factory Record SubPzRing_isSubComPzRing (R : comPzRingType) S U
    & SubPzRing R S U := {}.

HB.builders Context R S U & SubPzRing_isSubComPzRing R S U.
HB.instance Definition _ := SubSemiRing_isSubComSemiRing.Build R S U.
HB.end.

does not seem to be complete. The error is now:

Error:
HB: GRing.SubPzRing_isSubComPzRing.axioms_ is not a factory or its library (mathcomp.algebra.algebraic_hierarchy.ssralg.GRing) was not correctly imported

I tested locally and this is indeed the error one gets
when the addition is inside Module Ring./End Ring.
(without the Import).

Note that another way to make it work is to add
the factory between Module GRing. and End GRing. HB.export GRing.
or Module GRing. and End GRing. Export GRing.

I'll do more local checks unless somebody can spot the right fix.

[affeldt-aist]

This PR is a strict generalization, solving an issue, and MathComp master has been patch so that the CI is green (and more fixes/improvements are on their way on the MathComp side).

I will merge soon unless somebody spots a problem.