I am looking for a development defining finite support (sub)-probability distribution on an arbitrary type (in particular without decidable equality).

Is there any up to date library for doing proof about this kind of basic probability theory in Coq ? I am aware of ALEA but it seems rather outdated (Coq 8.3).

Have a look at classical analysis in math-comp. It will be merged with infotheo. However, neither of them is constructive, as you seem to require.
There is also FCF.

For completenes, here is a development by Pierre-Yves Strub on probability and probabilistic programs building on MathComp Analysis (which already has definitions of distributions and similar concepts):