When typing closed formulas, recast unification errors as typing errors.

[fix #17143]
`require` now takes a list of module.

[fix #17139]
Raise default timeout for the test-suite
In matching algorithm, add local binding to the env. when crossing a binder

This may be used by the conversion algorithm.

+ some refactoring.

[fix #17144]
Merge branch '1.0' of git://ci.easycrypt.info/easycrypt into 1.0