Bump the recommended OCaml version to 4.14.2 (master branch)

[meithecatte]

#250 ported to the master branch, as requested.

[mrhaandi]

Probably not related to the current PR, but there is a compile error:

  ROCQ compile FOL/TRAKHTENBROT/enumerable.v
  File "./FOL/TRAKHTENBROT/enumerable.v", line 133, characters 70-72:
  Error: Error: No such hypothesis: Hm

[DmxLarchey]

@mrhaandi

The compile error was due to a change in how destruct behaves on Section variables. Before, it was not removed but now it is.

There are other compile errors

ROCQ compile HOU/concon/conservativity_consequences.v
File "./HOU/firstorder.v", line 999, characters 70-99:
Warning: In term, tolerating this expression at a higher level than expected
by the notation continuing on the right (which is not left-associative). This
tolerance will be eventually removed. Insert parentheses or try to lower the
level at which the top symbol of this expression is parsed.
[level-tolerance,deprecated-since-9.2,deprecated,parsing,default]
File "./HOU/firstorder.v", line 1028, characters 15-31:
Error: decr_lambda_free depends on the section variable free but free in the
current context does not refer to the section variable of the same name.

possibly more annoying ...

[DmxLarchey]

@mrhaandi

Btw there are tons of warnings about rewrite being renamed as rw ... I do not know why such "cleanup" ideas pop up but they mess with this code base on a very large scale.

[meithecatte]

FWIW, the rewrite -> rw thing seems to be specifically about ssreflect's rewrite tactic – cf. rocq-prover/rocq#21478

[DmxLarchey]

Oh yes indeed, this to not apply to Ltac rewrite, thank god ;-)

[meithecatte]

I've pushed a fix for the error, the branch now compiles with Rocq-dev on my side.

[DmxLarchey]

@mrhaandi I am ok for a merge. Do you agree?

[mrhaandi]

@mrhaandi I am ok for a merge. Do you agree?

I agree.