Active fpa as default

[Halbaroth]

Activating FPA as default introduce a tiny time regression (about 1%) but we prove more goals on both ae-format and why3-gallery.

Fix issue #917

[bclement-ocp]

The documentation needs to be updated as well. Essentially we should revert most of #780.

[bclement-ocp]

We probably want to remove this bit of code as well, I think.

        Result.bind theories @@ fun theories ->
        if List.mem Theories.(Prelude Fpa) en then
          if List.for_all (fun th ->
              match (th : Theories.t) with
              | Prelude Nra | Prelude Ria -> false
              | _ -> true
            ) dis then
            Ok Theories.(Prelude Nra :: Prelude Ria :: theories)
          else
            Fmt.error_msg "theory prelude fpa requires both ria and nra"
        else Ok th

We no longer need to have --enable-theories fpa imply --enable-theories ria and --enable-theories nra (this was done only for convenience of users who would not have to list all 3 theories, but now they don't have to list anything at all).

We have said in the release meeting that we wanted to try updating CHANGES.md as we go; this would deserve an entry there.

[Halbaroth]

Actually, I hesitated to remove it but if you type --enable-theory fpa --disable-theories nra, ria, the current code will produce an error as this combination is forbidden.

[bclement-ocp]

As I stated above: this combination was forbidden in #780 because we wanted --enable-theories fpa to also automatically enable ria and nra for convenience. If we enable the fpa theory by default, we no longer need this convenience, and there is no reason to forbid this combination anymore.

[bclement-ocp]

I think the changelog entry is still missing and they we can merge