- annots order for multiple emitters is unspecified,
- use the order used in the Printer

[Wp] generic sequent simplifier: applies simplify+assume succesively on each terms of a the disjonctive goal

[Wp] generic sequent simplifier: applies simplify+assume succesively on eacterms of a the conjective hypothesis

- not available from GUI for now
- TacClear and TacUnfold adapted

- Rationale: detect RTE fail sooner

- A1 A2 ... : prove A1 -> hyp A1 -> prove A2 -> hyp A2 ...
- Move smoke tests to the end of code assertions

The term corresponding to the logic var introduced is translated without
the logic var in the logic scope.

- Replace `Env.with_rte` and `Env.with_params` to be able to set `rte`
and `kinstr` for an environment;
- Remove `kinstr` parameters from the `Contract` function to use the
`kinstr` of the environment instead;
- Setup environment `kinstr` when injecting code into a statement or
when translating code or function annotation.

Regarding `Translate_annots.pre_funspec` and
`Translate_annots.post_funspec`, since they only translate function
annotations, the `kinstr` is directly set to `Kglobal` in the functions
instead of being taken as a parameter.