Refactoring lebesgue measure and integral

[CohenCyril]

Lebesgue measure and integral (was: "refactor of intervals")
CC @affeldt-aist

closes #371
closes #492

[affeldt-aist]

That's all fine with (modulo the changelog update :-/).

[affeldt-aist]

The errors are syntax errors with Coq 8.13 only.
I fixed some in lebesgue_measure.v (by adding parentheses to disambiguate the parsing of intervals) but didn't have time to fix the ones in `lebesgue_integral.v":

# File "./theories/lebesgue_integral.v", line 1428, characters 53-54:
# Error: Syntax error: 'nnsfun' 'of' expected after '[' (in [term]).

[affeldt-aist]

The only errors are now "Nix CI for bundle" errors, so they are maybe not relevant.

[CohenCyril]

The only errors are now "Nix CI for bundle" errors, so they are maybe not relevant.

@affeldt-aist I fixed something in boolp.v doc, added some (working) nix CI, and we should be good to go.

[affeldt-aist]

Only one failure left:

Nix CI for bundle master / coq (pull_request_target)  Failing after 24s — coq

Checking presence of CI target coq

Run nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \
  nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \
     --argstr bundle "master" --argstr job "coq" \
     --dry-run 2>&1 > /dev/null)
  echo $nb_dry_run
  echo ::set-output name=status::$(echo $nb_dry_run | grep "built:" | sed "s/.*/built/")
  shell: /usr/bin/bash -e {0}
  env:
    tested_commit: dba57a6d631d8b2b199cc308d10a53590529fdea
    NIX_PATH: nixpkgs=channel:nixpkgs-unstable
Error: Process completed with exit code 1.

[CohenCyril]

The CI errors will disapear after the merge