[PPL-devel] [GIT] ppl/ppl(floating_point): Merge branch 'floating_point' of ssh://git. cs.unipr.it/git/ppl/ppl into floating_point